The λ-Cube(en.wikiversity.org)
en.wikiversity.org
The λ-Cube
https://en.wikiversity.org/wiki/Foundations_of_Functional_Programming/The_%CE%BB-cube
101 comments
I actually understood your article about the lambda cube much better. Also, very nice formatting and clean design, very readable on my phone.
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
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
No comments on the writing, but one thing to add: the syntax highlights for code get lost a bit. I would see them better either if they were a lighter black (aka dark grey), or had a different background than the rest of the text.
Do you mean the inline code or code blocks? In any case, I tweaked the background to be more different from the page background (in both light and dark mode) and also gave inline code that same background. Does that help?
https://github.com/azdavis/azdavis.net/commit/55199593abfb6e...
Yep, works for me
Thank you
Thank you
Cool stuff! How do I decipher the symbols that make up the equations for "application" and "abstraction"?
The definition I gave at the end of the article (the thing starting with `t ::=`) is basically a context-free grammar describing the syntax for terms of the calculus of constructions.
`t ::= ...` is saying "A CoC term, called t, can have the following forms ..." Then each case is separated by `|`.
The cases for application, abstraction, and forall are recursive, in that they contain t (or t') when the thing being defined is also called t. (The prime on t' is just to say that t and t' can be different terms.)
So for instance, the case for application is:
t(t')
That means if you already have two arbitrary CoC terms, called t and t', then if you write down first the term t, then a `(`, then the term t', then a `)`, then you've written down another CoC term representing the application of the term t to the term t'.
And the case for abstraction is
λ(x:t) t'
That means if you have two CoC terms t and t', then if you write down `λ`, then `(`, then a variable name (x is kind of a meta-variable-placeholder name, you can name the variable whatever you want), then `:`, then the term t, then `)`, then the term t', then you've written down an abstraction term. In this case, the variable x (or whatever you called it) has type t, and can appear free in t'.
`t ::= ...` is saying "A CoC term, called t, can have the following forms ..." Then each case is separated by `|`.
The cases for application, abstraction, and forall are recursive, in that they contain t (or t') when the thing being defined is also called t. (The prime on t' is just to say that t and t' can be different terms.)
So for instance, the case for application is:
t(t')
That means if you already have two arbitrary CoC terms, called t and t', then if you write down first the term t, then a `(`, then the term t', then a `)`, then you've written down another CoC term representing the application of the term t to the term t'.
And the case for abstraction is
λ(x:t) t'
That means if you have two CoC terms t and t', then if you write down `λ`, then `(`, then a variable name (x is kind of a meta-variable-placeholder name, you can name the variable whatever you want), then `:`, then the term t, then `)`, then the term t', then you've written down an abstraction term. In this case, the variable x (or whatever you called it) has type t, and can appear free in t'.
Awesome, thank you for the thorough explanation!
Very nice; you get to the practical lesson of it in a fairly straightforward manner while keeping interesting tangents where they aren’t distracting.
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.
> 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.
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.
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.
My understanding is that Javascript (for all its woes) is more nearly the untyped lambda calculus.
For example, you can do:
my_list.map(e=>(a=>some_transform(a)+some_other(a))(sanitize(e)))
or otherwise in LC:
(map my_list (\e (\a (add (some_transform a) (some_other a))) (sanitize e)))
Perhaps much of the power or even the success of javascript is that, in its own way, it brings us closer to the light.
It could be, with progressive typing systems (as attempted by TypeScript), with a coherent manner of synthesizing ground types (in the LC itself, subject to a kind of logical 'shield' as we might understand from Arduino), and a sensible conceptual model for dealing with side effects / threading, we could find a pure way of programmatic expression - allowing the model within our minds becomes reified once and for all.
Or, it could be that this ideal is unreachable in a fundamental sense.
For example, you can do:
my_list.map(e=>(a=>some_transform(a)+some_other(a))(sanitize(e)))
or otherwise in LC:
(map my_list (\e (\a (add (some_transform a) (some_other a))) (sanitize e)))
Perhaps much of the power or even the success of javascript is that, in its own way, it brings us closer to the light.
It could be, with progressive typing systems (as attempted by TypeScript), with a coherent manner of synthesizing ground types (in the LC itself, subject to a kind of logical 'shield' as we might understand from Arduino), and a sensible conceptual model for dealing with side effects / threading, we could find a pure way of programmatic expression - allowing the model within our minds becomes reified once and for all.
Or, it could be that this ideal is unreachable in a fundamental sense.
> 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.
If you add parametric polymorphism, you're not far from ML, which lives on these days as Standard ML and somewhat through OCaml.
Your conclusion is spot on.
The untyped lambda calculus is inconsistent.
If the guarantee you want from your system is consistency then you don’t want the untyped lambda calculus.
As software engineers who inherently understand system fragility as being an undesirable property we actually prefer para-consistent systems because they don’t “explode” under contradictions.
If the principle of explosion entails fragility; paraconsiatency entails anti-fragility.
The untyped lambda calculus is inconsistent.
If the guarantee you want from your system is consistency then you don’t want the untyped lambda calculus.
As software engineers who inherently understand system fragility as being an undesirable property we actually prefer para-consistent systems because they don’t “explode” under contradictions.
If the principle of explosion entails fragility; paraconsiatency entails anti-fragility.
An honest question - what is the problem with inconsistency in using lambda calculus as a programming language and not as foundation of mathematics?
"""The lambda calculus was introduced by mathematician Alonzo Church in the 1930s as part of an investigation into the foundations of mathematics.[7][a] The original system was shown to be logically inconsistent in 1935 when Stephen Kleene and J. B. Rosser developed the Kleene–Rosser paradox.[8][9]""" https://en.wikipedia.org/wiki/Lambda_calculus#History
"""The lambda calculus was introduced by mathematician Alonzo Church in the 1930s as part of an investigation into the foundations of mathematics.[7][a] The original system was shown to be logically inconsistent in 1935 when Stephen Kleene and J. B. Rosser developed the Kleene–Rosser paradox.[8][9]""" https://en.wikipedia.org/wiki/Lambda_calculus#History
Practically nothing.
By virtue of all programming being resource-bounded computations can be interpreted in Linear logic [1]. Linear logic is paraconsistent [2] not consistent.
Untyped Lambda calculus is essentially an assembly language and Assembly languages treat their own code as data [3]. Contradictions arrise when a system can mutate its own state. That is the power and pitfall of reflection [4]
[1] https://en.wikipedia.org/wiki/Linear_logic
[2] http://nlab-pages.s3.us-east-2.amazonaws.com/nlab/show/parac...
[3] https://en.wikipedia.org/wiki/Metaprogramming
[4] https://en.wikipedia.org/wiki/Reflective_programming
By virtue of all programming being resource-bounded computations can be interpreted in Linear logic [1]. Linear logic is paraconsistent [2] not consistent.
Untyped Lambda calculus is essentially an assembly language and Assembly languages treat their own code as data [3]. Contradictions arrise when a system can mutate its own state. That is the power and pitfall of reflection [4]
[1] https://en.wikipedia.org/wiki/Linear_logic
[2] http://nlab-pages.s3.us-east-2.amazonaws.com/nlab/show/parac...
[3] https://en.wikipedia.org/wiki/Metaprogramming
[4] https://en.wikipedia.org/wiki/Reflective_programming
> 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.
Difficult, but certainly not impossible [0].
[0] https://cakeml.org/
Difficult, but certainly not impossible [0].
[0] https://cakeml.org/
I'm not so sure most lisps are just a wrapper around untyped lambda calculus. The purely functional bits maybe more or less, but mutation and side effects are an integral part of at least scheme and common lisp.
Asking because I see something that's a lot of mappings with zero context: Why/ for what is the Lambda-Cube useful?
I think it's useful mostly as a sort of Linnæan 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.
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.
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.
The question was ‘why is the lambda cube useful?’
This answer was:
‘Assigning mathematical meaning.’
This is why people think these concepts aren’t useful, because this was a lot of words without any practical example of what it would be used for.
Here’s a practical example: there are type systems in the lambda cube that allow us to statically check that a list has a certain length. That means a compiler can prevent an out of bounds access error, without human intervention. I have written code that crashes because of an out of bounds access, so the idea is interesting to me.
This answer was:
‘Assigning mathematical meaning.’
This is why people think these concepts aren’t useful, because this was a lot of words without any practical example of what it would be used for.
Here’s a practical example: there are type systems in the lambda cube that allow us to statically check that a list has a certain length. That means a compiler can prevent an out of bounds access error, without human intervention. I have written code that crashes because of an out of bounds access, so the idea is interesting to me.
> This answer was:
> ‘Assigning mathematical meaning.’
No, you misread. The answer was
> The lambda cube is a way to systematically organize the space of type theories.
All of this was already meaningful before the lambda cube. The cube just organizes what we knew in a systematic way. It shows the relationships between the various systems that exist when they are differentiated on the features that describe their expressive power.
> ‘Assigning mathematical meaning.’
No, you misread. The answer was
> The lambda cube is a way to systematically organize the space of type theories.
All of this was already meaningful before the lambda cube. The cube just organizes what we knew in a systematic way. It shows the relationships between the various systems that exist when they are differentiated on the features that describe their expressive power.
You're mostly describing why dependent types are useful (in preventing an entire class of errors).
The lambda cube is useful in comparing and reasoning about the features of type systems across languages.
The lambda cube is useful in comparing and reasoning about the features of type systems across languages.
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...
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?
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) {...}' ?
Can you do 'MyType<n> foo(int n) {...}' ?
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.
You could do this with the factory pattern, applied to a template type. Though, if you would do this for the whole range of say, an int, you would probably blow up the compiler. How is that done in languages that do support this? Or does it require shipping the compiler, so that you can run the compiler at runtime?
> You could do this with the factory pattern, applied to a template type.
I don't know enough about C++ templates here, but you cannot in Rust.
> How is that done in languages that do support this?
I don't know enough about the implementations to actually say, to be honest. Most of them aren't systems languages, and so have significantly less constraints on implementations, and less monomorphization. I imagine that helps.
I don't know enough about C++ templates here, but you cannot in Rust.
> How is that done in languages that do support this?
I don't know enough about the implementations to actually say, to be honest. Most of them aren't systems languages, and so have significantly less constraints on implementations, and less monomorphization. I imagine that helps.
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.
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.
The syntax part seems to be missing most of the type constructors of Martin Lof Type Theory, with no apparent ways of expressing them:
More here: https://en.wikipedia.org/wiki/Calculus_of_constructions
Turns out they can be expressed after all.
- Dependent sum
- Cartesian product
- Disjoint union
More here: https://en.wikipedia.org/wiki/Calculus_of_constructions
Turns out they can be expressed after all.
Church constructions?
- Dependent sum
- Dependent sum
Sigma A (\x -> B) = (C : *) -> ((x : A) -> B x -> C) -> C
Pair A B = (i : Bool) -> (if i then B else A)
Sum A B = (C : *) -> (A -> B -> C) -> C
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.
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.
Is there a symbology primer for the lay reader who finds the Type Theory table at the bottom a trifle dense?
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.
[deleted]
Cut out and assemble yourself: https://www.irisa.fr/lande/ridoux/LPAZ/node47.html
Here's a website where you can try a few of these systems: https://typezoo.netlify.app/
So what is a "type", according to this formalism?
Isn't it a function from any value you can create in a programming language to Boolean result which tells if that value is a member of that type?
Isn't it a function from any value you can create in a programming language to Boolean result which tells if that value is a member of that type?
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.
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) λ-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
> 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) λ-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
> 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) λ-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".
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) λ-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".
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.
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.
Java uses sum types for “result or error”. Exceptions just make it a language-level construct, with automatic addition of very useful stacktraces, auto-unwrap in the “result” case, etc.
Parametric polymorphism is even older than that! It's almost 60 years old, having originated in CPL.
> 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.
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.
> 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.
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.
> 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.
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.
IMO there is also 'culture' to various programming languages in their styles, standard libraries and so on. I think Java as language is actually fine, it's all the crap that surrounds it that makes it more unproductive or not. I find my self even once I get past 2000 lines that using something like python is less productive than a statically typed language.
> 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.
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.
> 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.
I do think there's been a "type renaissance" in the past 5 or so years, after we all dove headfirst into JS and Python and broke the whole internet.
I do think there's been a "type renaissance" in the past 5 or so years, after we all dove headfirst into JS and Python and broke the whole internet.
Yeah, I agree. I think part of it is due to embracing better type systems. For example TS and Go are structurally typed, which was a rarity before. Type inference is everywhere now. Sum types are usable in Java, TS, Rust. All of these languages are better than 2005 Java. Maybe we'll have a comeback of dynamic languages in the next 5-15 years, and if that's the case I'd love to see what people will come up with.
> > 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.
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.
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?
> 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.
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.
"Typing is Hard" is a popular list of languages and the decidability of typechecking in them: https://3fx.ch/typing-is-hard.html
That's a nice list
> Zig
> undecidable, since evaluation of recursive functions at compile time is possible, thus requiring the compiler to solve the halting problem.
For some reason, I find that amusing.
> Zig
> undecidable, since evaluation of recursive functions at compile time is possible, thus requiring the compiler to solve the halting problem.
For some reason, I find that amusing.
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.
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.
Go is the poster boy for a language NOT learning anything from decades of PL theory and research.
In my mind, Go is an attempt at keeping the nice things about Java while discarding the worse things.
Then they have a very strange definition of nice things, when it includes worse error-handling, more verbosity and bad abstractibility.
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'.
TypeScript is language that allows you to work like that. You may use as many and as few types as you need at any given stage of development.
As you start adding types to your working program compiler debugs your program for you finding various corner cases.
This motivates you to add more types.
As you start adding types to your working program compiler debugs your program for you finding various corner cases.
This motivates you to add more types.
Yea, it is indeed how I use typescript, but I do not really like javascript much. Typescript does make it better though. I wish other, nicer languages had this.
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.
While making constructive mathematics rigorous was Martin-Löfs 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...
[0]: 1982 version: https://raw.githubusercontent.com/michaelt/martin-lof/master...
I’m aware of math being entirely useful outside of programming - my little rant is more about how little programming is inspired by math
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.
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.
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.
> 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.
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.
I have been wondering why programming is so much more accessible than mathematics to many, considering programming is in some way also a kind of mathematics.
I think some of it may have to do with the fact that in programming, one can get immediate and non-judgmental feedback about the correctness of ones solution. In mathematics, it's usually a lot more difficult to verify a solution if you don't already know the answer, so you're dependent on people for it.
So perhaps, interactive theorem provers may make mathematics a lot more accessible. But I hope the art of doing it with pen and paper doesn't get lost on us with it.
I think some of it may have to do with the fact that in programming, one can get immediate and non-judgmental feedback about the correctness of ones solution. In mathematics, it's usually a lot more difficult to verify a solution if you don't already know the answer, so you're dependent on people for it.
So perhaps, interactive theorem provers may make mathematics a lot more accessible. But I hope the art of doing it with pen and paper doesn't get lost on us with it.
It's a controversial but good opinion. Mathlib marches on and gets better and better.
> a proof development system, aka dependently typed programming language.
There are proof assistants without dependent types, like Isabelle/HOL.
There are proof assistants without dependent types, like Isabelle/HOL.
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.
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.
> 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.
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)
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.
The two main hurdles with dependent types are:
- Type-checking is undecidable. I've not found that to be much of a problem, since it can be given a timeout (or hit Ctrl-C).
- Soundness requires functions to be total (either terminating or co-terminating). That's generally a good idea anyway, but the approaches for doing this aren't particularly great; e.g. structural recursion is simple to implement and understand, but is very restrictive.
Idris makes the pragmatic choice of allowing the totality-checker to be turned off on a per-function basis; which is certainly no worse than using a language with no totality checking.
Another approach I've enjoyed using is Mtac in Coq: general recursion is an effect, which gets wrapped in a type (similar to Haskell's IO); there is an unwrapping function (like unsafePerformIO) but it gets executed at compile-time, so non-total functions create an infinite loop at compile time (rather than at runtime).
- Type-checking is undecidable. I've not found that to be much of a problem, since it can be given a timeout (or hit Ctrl-C).
- Soundness requires functions to be total (either terminating or co-terminating). That's generally a good idea anyway, but the approaches for doing this aren't particularly great; e.g. structural recursion is simple to implement and understand, but is very restrictive.
Idris makes the pragmatic choice of allowing the totality-checker to be turned off on a per-function basis; which is certainly no worse than using a language with no totality checking.
Another approach I've enjoyed using is Mtac in Coq: general recursion is an effect, which gets wrapped in a type (similar to Haskell's IO); there is an unwrapping function (like unsafePerformIO) but it gets executed at compile-time, so non-total functions create an infinite loop at compile time (rather than at runtime).
> Type-checking is undecidable.
This is only true if you allow non-total functions in your types, which most dependently-typed languages don't by default (i.e. the condition implied by your soundness condition).
By default in e.g. both Idris and Agda type-checking is decidable.
This is only true if you allow non-total functions in your types, which most dependently-typed languages don't by default (i.e. the condition implied by your soundness condition).
By default in e.g. both Idris and Agda type-checking is decidable.
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.
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.
If I understood the article correctly the four type of functions are present in Julia:
> 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
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})
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
> 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
I am no expert on the topic but pretty much every language has an instanceof-like pattern — that doesn’t really fulfill the generic term-to-type capability in my opinion. That would be being able to create a new type at runtime from a term based on a user-defined function — which yet again may have some constraints like only compile-time known constants can be used, etc.
I don’t know the peculiarities of julia to comment on this specific language though.
I don’t know the peculiarities of julia to comment on this specific language though.
Also not an expert, or even educated on it.
In the case of Julia for example static arrays can be created, at runtime or not, with a fixed length that is part of the type definition, to give a less trivial example than "is an instance of". It's actually a very practical example as static arrays are of great importance for performance on certain applications.
I think most people would dismiss dynamic language examples, and that's the reason I comment Julia is dynamic in my comment, because most people interested in types are interested in using them at compile time to prove, or strengthen at least, correctness. In the case of dynamic languages types feel like just another piece of metadata and if you have "eval" available you basically can do anything. Julia actually does not use types to catch bugs but to structure programs and to improve performance when possible (to great extent).
In the case of Julia for example static arrays can be created, at runtime or not, with a fixed length that is part of the type definition, to give a less trivial example than "is an instance of". It's actually a very practical example as static arrays are of great importance for performance on certain applications.
I think most people would dismiss dynamic language examples, and that's the reason I comment Julia is dynamic in my comment, because most people interested in types are interested in using them at compile time to prove, or strengthen at least, correctness. In the case of dynamic languages types feel like just another piece of metadata and if you have "eval" available you basically can do anything. Julia actually does not use types to catch bugs but to structure programs and to improve performance when possible (to great extent).
Again, only superficially knowing julia, in what way is this static array a type over being a value as it is in java, with having a field with the length (the type being the x[] only, without length)?
It's a good question. Intrinsically, there is no difference: you need to consider how both pieces of data are used. Consider these two "equivalent" 1D arrays:
Off tangent, but these reminds me the first time I read the phrase "everything in Python is an object". That got me puzzled because in my mind if "everything is an object" then the phrase has zero information content. You cannot understand what is an object in isolation, you need to consider how the interpreter uses them. Or the first time you try understand what is a vector in mathematics. You cannot understand a vector in isolation, you need to consider the vector space it lives in, what operations are allowed.
x = Vector{Float64}(1, 2, 3)
y = SVector{3, Float64}(1, 2, 3)
Off tangent, but these reminds me the first time I read the phrase "everything in Python is an object". That got me puzzled because in my mind if "everything is an object" then the phrase has zero information content. You cannot understand what is an object in isolation, you need to consider how the interpreter uses them. Or the first time you try understand what is a vector in mathematics. You cannot understand a vector in isolation, you need to consider the vector space it lives in, what operations are allowed.
Without any authority, I really don’t see how is it any different from any language’s arrays vs lists. I feel like it is syntax only for the age-old “let’s store the size of the array next to the data” vs a more complicated implementation like std::vector or Java’s ArrayList which may copy the content into a new, larger array behind the scenes.
So it is probably meaningless to talk about it in case of dynamically typed languages, even though type enforcement may not be needed (as it is impossible in the generic case for dependent types)
So it is probably meaningless to talk about it in case of dynamically typed languages, even though type enforcement may not be needed (as it is impossible in the generic case for dependent types)
To turn the question around, what _would_ make it part of the type in your opinion, what criterion do you use to distinguish that from "having a field with the length (the type being the x[] only, without length)"?
There is a huge disconnect between industry and academia. Type systems are very interesting but is not what makes the difference in industry. What actually increases productivity and reduces bugs is an under explored area. I think the answers are just as much about sociology, psychology, and ergonomics as they are about type theory.
As with all research, the good ideas eventually make it to production.
[deleted]
I’ve been using my website as a way to practice writing, so please let me know what you think.