[HN Gopher] The l-Cube
___________________________________________________________________
The l-Cube
Author : todsacerdoti
Score : 106 points
Date : 2022-01-15 18:25 UTC (4 hours ago)
(HTM) web link (en.wikiversity.org)
(TXT) w3m dump (en.wikiversity.org)
| dataangel wrote:
| Can anyone ELI5 the difference between dependent types and what
| Rust calls const generics and what C++ calls non-type template
| parameters? If I have a type that is templates/generic on an
| integer value, e.g. 'MyType<3>' is that a dependent type?
| drdeca wrote:
| If that 3 can be decided at runtime rather than at compile
| time, yes.
|
| Like, if I can have a type Array<Type,Length> and have a
| function f which has as its input type Int, with the name of
| the input variable being n, and as its return type
| Array<Bool,n> and when you give the return value to something
| else, it checks (at compile time) that the length of the array
| (i.e. , n ) matches what the other thing is expecting,
|
| that would be using dependent types.
| steveklabnik wrote:
| They're subsets of true dependent types, in my understanding.
| This is because they can only do this at compile time, not
| runtime. There's no way to say, get a number over stdin, put it
| in a variable n, and then instantiate MyType<n> with that
| variable. You can with true dependent types.
| codebje wrote:
| A dependent type is a function from a value to a type - where a
| value is a runtime value, not a compile time constant.
|
| Can you do 'MyType<n> foo(int n) {...}' ?
| smitty1e wrote:
| Is there a symbology primer for the lay reader who finds the Type
| Theory table at the bottom a trifle dense?
| [deleted]
| mdm12 wrote:
| You, my friend, are diving into the realm of formal semantics
| for programming languages. Benjamin Pierce's Types and
| Programming Languages is an excellent reference, but it is not
| for the faint of heart.
| abeppu wrote:
| Maybe a twist on the "why is this useful" question ...
|
| Users of lisp often are enthusiastic about the idea that lisp is
| at its core a minimal wrapper around the untyped lambda calculus
| (e.g. plus naming, primitive values and operations, etc).
|
| Why do we not generally see languages which are minimal wrappers
| around these typed lambda calculi? Perhaps intermediate languages
| are built closely around these formal systems (e.g. I'm aware
| that Haskell Core is closely based around System FC), but
| languages which are intended for human authors and readers seem
| to introduce a lot of extra machinery. Why is that?
|
| One guess is that lisps cope with being minimal through use of
| macros and metaprogramming, it's difficult for a typed language
| to support that level of metaprogramming while maintaining the
| various guarantees that one wants from such a system.
| Zababa wrote:
| > Why do we not generally see languages which are minimal
| wrappers around these typed lambda calculi?
|
| If you add parametric polymorphism, you're not far from ML,
| which lives on these days as Standard ML and somewhat through
| OCaml.
| vilhelm_s wrote:
| Cut out and assemble yourself:
| https://www.irisa.fr/lande/ridoux/LPAZ/node47.html
| azdavis wrote:
| I actually wrote a bit about this on my website:
| https://azdavis.net/posts/lambda-cube/
|
| I've been using my website as a way to practice writing, so
| please let me know what you think.
| AlexSW wrote:
| Nothing to add to the other comments, just wanted to add
| another data point that the website (on mobile) was perfectly
| clear and the information was all laid out and explained very
| well; I have no (constructive) criticism to give.
| azdavis wrote:
| Thank you!
| wlib wrote:
| Very nice; you get to the practical lesson of it in a fairly
| straightforward manner while keeping interesting tangents where
| they aren't distracting.
| azdavis wrote:
| I really appreciate your feedback, thank you!
|
| > interesting tangents
|
| Yeah, I've found that explaining things by first giving an
| example and then generalizing often works better than trying
| to start with raw theory.
| kinow wrote:
| Great post! I was going to share this one on the
| r/functionalprogramming subreddit when I found yours. A lot
| easier to read, and helps reading the Wikiversity afterwards.
| Thanks!
| azdavis wrote:
| Wow thanks! Never had my stuff shared out before to my
| knowledge but I appreciate it! I'll take a look :D
| plafl wrote:
| I actually understood your article about the lambda cube much
| better. Also, very nice formatting and clean design, very
| readable on my phone.
| azdavis wrote:
| Thank you! I've tried to make sure that my site reads well
| and loads fast, even on mobile.
|
| There's actually no JS on my site at load time, I run it all
| as a build step that transforms Markdown with inline LaTeX
| into pure HTML and CSS.
| https://github.com/azdavis/azdavis.net
| ogogmad wrote:
| The syntax part seems to be missing most of the type constructors
| of Martin Lof Type Theory, with no apparent ways of expressing
| them: - Dependent sum - Cartesian product
| - Disjoint union
|
| [edit]
|
| More here:
| https://en.wikipedia.org/wiki/Calculus_of_constructions
|
| Turns out they can be expressed after all.
| remexre wrote:
| Church constructions?
|
| - Dependent sum Sigma A (\x -> B) = (C : *)
| -> ((x : A) -> B x -> C) -> C
|
| - Cartesian product Pair A B = (i : Bool) ->
| (if i then B else A)
|
| - Disjoint union Sum A B = (C : *) -> (A -> B
| -> C) -> C
|
| EDIT: Ah, started writing before you edited; yeah, (with an
| expressive enough type system) lambda's all you need
| atennapel wrote:
| Your `Sum` is actually a `Pair` as well :). Should be: ```
| Sum A B = (C : *) -> (A -> C) -> (B -> C) -> C ```
|
| Note that in the calculus of constructions you can do these
| Church encodings of datatypes but you cannot derive an
| induction principle for these (only non-dependent folds). For
| example you cannot write a `snd` for the `Sigma` above.
|
| As you allude to, you need a more expressive type system to
| derive induction principles (for example "Self types") for
| lambda encodings.
| neilkakkar wrote:
| Asking because I see something that's a lot of mappings with zero
| context: Why/ for what is the Lambda-Cube useful?
| viewfromafar wrote:
| Type theories are formal logic languages. People use formal
| logic for all sorts of things but mathematics has the longest
| history. This is where people first defined formal languages
| and assigned meaning (mathematical meaning.)
|
| Starting from simply typed lambda calculus ("simple type
| theory", also "higher order logic"), one can make various
| extensions that make the logic language more expressive. The
| lambda cube is a way to systematically organize the space of
| type theories.
|
| Interestingly, the theory has become very relevant for type
| systems of normal programming languages. Milner invented ML as
| "meta language" for helping with logic and theorem proving, but
| it was used widely and today everyone expects generics to work
| more or less as in System F polymorphic lambda calculus.
| JadeNB wrote:
| I think it's useful mostly as a sort of Linnaean classification
| device--it's a lot easier to compare different type systems by
| placing them on a 'standard' cube, than by choosing ad hoc
| points of comparison.
| viewfromafar wrote:
| For anyone who wants to dive deeper, this a good series of short
| video lectures pulled together by students of TU Berlin that
| introduces this topic:
| https://youtube.com/playlist?list=PLNwzBl6BGLwOKBFVbvp-GFjAA...
| wlib wrote:
| Somewhat unrelated to this link, but I really think that it's
| interesting how much effort we put into the theory side of
| languages/types - with almost no one in industry applying these
| lessons. The essence of this is just something along the lines of
| "What if we unified values with types, so we could have more
| useful type checking?" We have billions of dollars being spent
| and thousands of smart people working for decades, who don't even
| get to use a proper type system - forget about statically-checked
| polymorphism or dependent typing. It's not even as if we lost the
| ball, we're running in the wrong direction. It's almost trivial
| to bolt on gradual typing to a language. It's also not too hard
| to retrofit dependent types (just don't bother with Turing-
| incompleteness). The whole point of these type systems is to
| better model systems, so why not go the extensible route of
| letting anyone hook into the "type checking" phase? Import affine
| types (that decades old thing that got rust popular); write your
| own domain-specific checker, even. It's so frustrating to see how
| beautiful ideas just die because we feel comfortable the way
| things are now. Maybe language was the wrong abstraction to begin
| with. Sorry to derail, but this feels like the only path to truly
| popularize the lambda cube as a concept.
| [deleted]
| ogogmad wrote:
| Type theory has uses outside programming. It can be used to
| make constructive logic rigorous, which was in fact Martin
| Lof's original use for it.
| wlib wrote:
| I'm aware of math being entirely useful outside of
| programming - my little rant is more about how little
| programming is inspired by math
| exdsq wrote:
| I've used Haskell for 18 months in a professional setting.
| I prefer C++. Grass is always greener - having endless
| abstractions to be mathsy becomes a real pain when you're
| trying to build real products.
| black_knight wrote:
| While making constructive mathematics rigorous was Martin-
| Lofs original goal, he was quite early aware of the
| applications to computer science. See for instance his
| 1979ish paper <<Constructive Mathematics and Computer
| Programming>>[0]
|
| [0]: 1982 version:
| https://raw.githubusercontent.com/michaelt/martin-
| lof/master...
| adamnemecek wrote:
| As with all research, the good ideas eventually make it to
| production.
| dvt wrote:
| You said a lot of stuff, and I disagree with most of it, but
| I'm open to dialogue.
|
| > with almost no one in industry applying these lessons
|
| Straight-up incorrect. Language designers think long and hard
| about how typings work in their languages. Rob Pike, Ken
| Thompson, and Russ Cox deliberated generics for like a
| decade[1] before finally allowing them in Go.
|
| > a proper type system
|
| I'm not sure exactly what you mean by "proper" -- but "rigid"
| type systems are extremely cumbersome to use practically.
| (Typed) l-calculus is an academic example; Haskell is a real-
| world example.
|
| > not too hard to retrofit dependent types (just don't bother
| with Turing-incompleteness)
|
| Hard disagree. It actually _is_ extremely hard: type resolution
| is undecidable, for one. So you need to carefully design type
| resolution in a way that the "edges" of types don't (or can't)
| break the runtime _too_ badly.
|
| > why not go the extensible route of letting anyone hook into
| the "type checking" phase
|
| Absolutely terrible idea, for many reasons, but mainly because,
| if C/C++ macros are any indication, people will abuse any kind
| of compile-time (or pre-processing) trickery you give them
| access to.
|
| > write your own domain-specific checker, even
|
| I guess I'm in the opposite camp here, I think domain specific
| languages are an absolute dumpster fire of abstraction and
| 99.9% of the time completely exceed the scope of the problem
| they're trying to solve. The purpose of a programming language
| is to be applicable to many classes of problems, and DSLs fly
| in the face of that pretty common-sense tenet.
|
| [1] https://research.swtch.com/generic
| wlib wrote:
| I'm on my phone so I can't really give this the response that
| it's owed, but most of what I want to say is that I don't
| think we disagree as much as you think. My mention of
| languages being the wrong approach to general programming is
| a key aspect of my position. You're right that DSL's are
| usually not a great idea, but that seems like more of an
| issue with the "syntax-chasing". The affordances that a
| syntax forces upon everyone are why it takes a decade to add
| generics to Go and why macros are even used to begin with. As
| we see from the various notations used for equivalent math,
| we probably we be better off encoding the structure as a
| flexible semantics graph and then "projecting the syntax"
| however the programmer wants. Keep in mind that what I write
| is about possibilities more than what you would be forced to
| do every project. You wouldn't expect everyone to import
| random type systems more than you would expect everyone of
| write and import their own random crypto system libraries.
| Some of the most popular languages out there have absolutely
| zero static checks. Would it be so bad to write a Turing
| complete static check function? Why do we care so much about
| decidability that we can't even consider it in useful
| exceptions? Also, do you think macros a la lisp would be so
| bad if they had more powerful type systems backing them up
| and more flexible editors to understand them?
| dvt wrote:
| > Would it be so bad to write a Turing complete static
| check function?
|
| I think most type systems are, in fact, Turing complete
| (there's a fun proof somewhere that TypeScript is, for
| example). And most typed languages (Go, C++, Java,
| TypeScript) have pretty mature static type-checkers, unless
| I'm misunderstanding your ask.
| foobiekr wrote:
| Oh my goodness do I ever agree about any kind of "use parser
| cleverness to make your cute interior domain specific
| language" thing as found in Scala and Ruby and a few other
| contexts.
|
| If you want a language, and have legit need, fire up antlr
| and build a quick compiler.
|
| Parser cleverness if the "internal DSl" variety is on par
| with the C++ windowing libraries that used heavy operator
| overloading to be clever, the stuff like "window += new
| Button()" and other nonsense. Just awful and torturous.
| rowanG077 wrote:
| Go is the poster boy for a language NOT learning anything
| from decades of PL theory and research.
| ebingdom wrote:
| > Straight-up incorrect. Language designers think long and
| hard about how typings work in their languages. Rob Pike, Ken
| Thompson, and Russ Cox deliberated generics for like a
| decade[1] before finally allowing them in Go.
|
| I think that kind of proves their point. Parametric
| polymorphism is one of the most well-understood, least
| contentious extensions to the lambda calculus. It's
| formalized by System F and has been implemented in
| programming languages 40 years ago with great type inference
| for an important subset (Hindley-Milner). Yet generics was
| highly controversial in the Go community. And now since none
| of the standard library was designed with generics in mind,
| it's full of unsafe patterns that involve essentially dynamic
| typing (e.g., the `Value` method of `Context`).
|
| Despite Rob Pike et al. designing one of the most popular
| languages today (Go), I consider them more experts in systems
| rather than programming languages.
|
| > I'm not sure exactly what you mean by "proper" -- but
| "rigid" type systems are extremely cumbersome to use
| practically. (Typed) l-calculus is an academic example;
| Haskell is a real-world example.
|
| I find Haskell a joy to use, and I cringe at having to use
| languages like Java and Go, which are a minefield of error-
| prone programming patterns (like using products instead of
| sums to represent "result or error"). Generally speaking, my
| Haskell code is shorter, less buggy, and more reusable than
| my Go code, so I'm not sure what you mean by "cumbersome".
| dvt wrote:
| > I find Haskell a joy to use, and I cringe at having to
| use languages like Java and Go, which are a minefield of
| error-prone programming patterns (like using products
| instead of sums to represent "result or error"). Generally
| speaking, my Haskell code is shorter, less buggy, and more
| reusable than my Go code, so I'm not sure what you mean by
| "cumbersome".
|
| I just want you to realize that you are in the _extreme_
| minority here, but just from a common-sense POV, if I 'm
| prototyping a project, looking for product-market fit, the
| last thing I want to care about is that my typeability is
| recursively enumerable or what-have-you. I just want to
| build something quickly without much hoopla (hence the
| massive popularity of very weakly-typed languages like JS
| and Python).
|
| FWIW, I think that generics are a mistake in Go, but I was
| just trying to counter the point that language designers
| don't think long and hard about type-theoretic features. I
| think the main issue with generics, wasn't so much an inept
| "we don't know how to do this," but rather "is this worth
| the code complexity?" and "is this worth the added compile
| times?" -- both of which were main selling points of Go.
| Zababa wrote:
| > I just want you to realize that you are in the extreme
| minority here
|
| Considering how much people love and use Rust, Typescript
| and typechecking in Python, I don't think your point
| about people prefering JS and Python is that strong.
| There is one thing that's sure: people hate typing Car
| car = new Car(). var car = new Car()? That's already
| better. Python and JS got popular in reaction to
| Java/C#/C++, which were painful to use. Even Go now has
| type inference, which helps a lot. Now in 2022 it's not
| the same as 2005. You can have static types and a fast
| time to market. Before thinking about dynamic vs static,
| we should first try to see what the best dynamic and
| static typing schemes we can come up with.
|
| > if I'm prototyping a project, looking for product-
| market fit, the last thing I want to care about is that
| my typeability is recursively enumerable or what-have-you
|
| That's a bit of a strawman. If I'm prototyping a project,
| the last thing I want to care about is the weird API
| design that the author of that library I need came up
| with, instead of just implementing a common interface.
| Python and JS both have iterators for a reason. People in
| the functional world talk about monads all the time for a
| reason too: it's a general interface that allows you to
| write code fast. Nullable code is the same as async code,
| is the same as iteration (well, mapping) code, is the
| same as parsing code.
| youerbt wrote:
| > > just from a common-sense POV, if I'm prototyping a
| project, looking for product-market fit, the last thing I
| want to care about is that my typeability is recursively
| enumerable or what-have-you.
|
| Then don't. It's not like Haskell forces you to, that's a
| myth about Haskell. You can get away with strings and
| integers everywhere if you so fancy.
|
| There is just no common-sense in thinking that computer
| assisted programming is slower than unassisted.
| ebingdom wrote:
| > I just want you to realize that you are in the extreme
| minority here
|
| I'm in the minority because I've spent an unusual amount
| of time investing in my understanding of programming
| languages and their features, not because I have some
| fringe unjustified opinion.
|
| > if I'm prototyping a project, looking for product-
| market fit, the last thing I want to care about is that
| my typeability is recursively enumerable or what-have-
| you.
|
| With this comment you've lost your credibility in my
| mind. No one actually goes through this train of thought.
| I don't wonder about recursive enumerability whenever I
| start a project. I just use tools that help me build high
| quality software, such as principled static type systems.
| dvt wrote:
| > I'm in the minority because I've spent an unusual
| amount of time investing in my understanding of
| programming languages and their features, not because I
| have some fringe unjustified opinion.
|
| I was just making a statement of fact. You're probably a
| very good programmer (as most _type nerds_ , to coin a
| new term, tend to be), but still in the minority. Most
| programmers are not very good, and even good ones
| sometimes want to build things fast. (Where type
| ambiguity or even incorectness is accepted as a viable
| trade-off.)
|
| This is why I stopped prototyping in Java, for example.
| JS just let me "do stuff" without thinking about it too
| hard. Lower code quality? Of course; but it let me try
| out more ideas in the same amount of time. Should you use
| JavaScript to write the operating system of a pacemaker?
| Probably not.
| obviouslynotme wrote:
| This is because type checking is the least impactful part
| of generics. As you said, that is a solved problem. The
| reason Go took so long thinking about generics has to do
| with their code generation. There are steep tradeoffs in
| compilation vs run time as well as compiler complexity and
| language complexity in general. Go's purpose was to be very
| fast to compile and run, born in a company where compile
| times for several projects run for hours even with massive
| parallelization.
|
| There is very good reason that Go's initial compromise was
| to use built-ins for a small number of highly useful
| generics like arrays and maps.
| tluyben2 wrote:
| This is what I have noticed writing a lot of software
| communicating with systems (old systems) with not very well
| specified input & output; I first want to write drivel and make
| it work. I don't want to write/change 1000s of vars/fields
| while i'm not sure if I even need them etc. Then I want to
| throw away and refactor with lessons learned and I want to keep
| doing that, adding types (and sometimes proofs). Maybe with
| compiler flags which enforces static typing for the 'production
| version'.
| shrimpx wrote:
| A core problem is that you don't need super fancy type systems
| to build robust systems in practice. After a certain threshold,
| type theory research is exploring what's possible in theory,
| like pure mathematics, not what would be good for
| practitioners.
|
| But one area of large impact for this pure type theory research
| seems to be the mechanization of mathematics. It looks probable
| that in the future, the standard way to do mathematics will be
| by programming it in a proof development system, aka
| dependently typed programming language.
| ogogmad wrote:
| > It looks probable that in the future, the standard way to
| do mathematics will be by programming it in a proof
| development system, aka dependently typed programming
| language.
|
| This is a controversial opinion, and not all mathematicians
| are enthusiastic about it, whether rightly or wrongly.
| Michael Harris, for instance, is a major sceptic and
| opponent.
|
| It is still a very interesting idea. And it has had some
| notable successes already.
| armchairhacker wrote:
| Most of the less abstract parts of this research (generic and
| polymorphic types w/ variance, ADT structs/unions, even type
| functions) are in most modern languages (Scala, TypeScript,
| C++20, Kotlin, Swift, Go). Rust even has affine types
|
| The more abstract parts like dependent types are _really_
| complicated and even unintuitive to use. See: issues with
| Rust's borrow checker, or Haskell being so confusing.
|
| Earlier languages like C and Java are mostly legacy code, they
| use libraries in legacy code, or they're for developers
| familiar with them.
|
| Untyped scripting languages are fine for scripts. Honestly idk
| why developers write big libraries in untyped languages like
| JavaScript and Python.
|
| The main case where advanced formal methods are particularly
| useful is proving program correctness. And AFAIK this stuff
| _is_ used by industry, although you don't hear about it as
| much. The thing is, most programs either don't "need" to be
| proved, or they're way too big.
| dwohnitmok wrote:
| Dependent types aren't terribly complicated intrinsically,
| see e.g. https://shuangrimu.com/posts/language-agnostic-
| intro-to-depe... for one explanation of dependent pairs.
|
| Nor do I think the value of dependent types comes from
| proofs, which I agree are still too cumbersome to really use
| at a large scale for most codebases.
|
| My hypothesis for the sweet spot for dependent types is to
| express invariants, and then use other mechanisms such as
| property tests to check those invariants, rather than actual
| proofs (except for trivial proofs). This does mean that I
| favor a very proof irrelevant style of dependently typed
| programming (i.e. in the language of Agda, way more `prop`
| than `set` or in Idris lots of zero multiplicities for
| dependently typed arguments) which is quite different from
| the way a lot of current dependently-typed code is written.
| plafl wrote:
| If I understood the article correctly the four type of
| functions are present in Julia: julia>
| factorial(3) # term -> term 6 julia> typeof(3) #
| term -> type Int64 julia> one(Float32) # type ->
| term 1.0f0 julia> Vector{Float32} # type -> type
| Vector{Float32} (alias for Array{Float32, 1})
|
| And actually more mixed: julia> using
| StaticArrays julia> SVector{3, Float32}(1, 2, 3)
| 3-element SVector{3, Float32} with indices SOneTo(3):
| 1.0 2.0 3.0 julia> convert(Float32, 1)
| 1.0f0
|
| Julia is of course dynamic, so maybe it's cheating? I'm
| writing this comment because all the greek in that cube, and
| actually using a cube, makes this look like very abstract
| stuff but I consider Julia a _very_ practical language.
|
| > Untyped scripting languages are fine for scripts. Honestly
| idk why developers write big libraries in untyped languages
| like JavaScript and Python.
|
| And yet it works
| chriswarbo wrote:
| > The more abstract parts like dependent types are really
| complicated and even unintuitive to use.
|
| I disagree with this: dependent types are _way_ easier than
| lots of the convoluted schemes that non-dependent languages
| have come up with.
|
| As a simple example, dependently-typed languages don't need
| parametric polymorphism or generics: we can achieve the same
| thing by passing types as arguments; e.g.
| map: (inType: Type) -> (outType: Type) -> (f: inType ->
| outType) -> (l: List inType) -> List outType map
| inType outType f l = match l with Nil inType
| -> Nil outType Cons inType x xs -> Cons outType (f
| x) (map inType outType f xs)
|
| When I program without dependent types, I regularly find
| myself getting "stuck" inadvertently; knowing that (a)
| there's no way to make my current approach work in this
| language, (b) that it would be trivial to make it work if I
| could pass around types as values, (c) that I need to throw
| away what I've done and choose a different solution, and (d)
| the alternative solution I'll end up with will be less
| correct and less direct than my original approach (e.g.
| allowing more invalid states)
| andrewflnr wrote:
| Is there work on cleanly subsetting dependently typed
| languages to ones where well-typed-ness can be
| automatically proven? That's not generally the case, right?
| I think those concerns are basically why people come up
| with less-general typing mechanisms.
___________________________________________________________________
(page generated 2022-01-15 23:00 UTC)