The lambda calculus is simple. It consists of only four essential things, and with those four things we can compute anything that is computable. (I don't claim that the lambda calculus is simple to understand — certainly there are people who have a hard time grasping it. But that's a different issue.)
What the author is doing is not "the lambda calculus"; it's an extended lambda calculus for dependent types. That's a huge step in terms of complexity. Yes, it might be the simplest lambda calculus for the task (I didn't check), but that is not at all "how to keep lambda calculus simple". Just a very odd choice for a title, in my opinion.
The Author is _not_ implementing dependent types. They specifically are implementing Simply Typed Lambda Calculus. They have stripped out the Pi and Sigma types from the original paper.
The original paper also does plain STLC first in section 2, and then adds dependent types in section 3. (And finally it adds the naturals in section 4.)
In the Idris2 github repository, Guillaume Allais goes a step further and shows a well-named version. There the types of terms and values are indexed by the list of names in the environment and the compiler checks that the manipulation of deBruin levels and indices is correct:
Very interesting blog, but also kind of hilarious that a post about keeping a concept "simple" proceeds with a dump of insanely long, dense, esoteric code, variable names and jargon.
I love functional programming and have had some fun diving deep into some of the underlying category theory concepts at times, but I feel like 95% of the time trying to introduce these advanced concepts into a practical, professional codebase will lead to severe headache.
I don't think your conclusion is especially fair. This is a blog post about programming language design and type theory not general usage of functional programming.
I wasn't really meaning to criticize the blog post. It's very intelligent and interesting. I just think the title is kind of silly and highlights how extremely complicated and impractical advanced functional programing theory and concepts can be if this is meant to present them in a "simple" way.
Perhaps I'm slightly misinterpreting the usage of "simple" here and it's related to the more technical notion of simply typed lambda calculus.
The techniques present in the paper and blog post are not really from functional programming but from mathematics. Functional programming just happens to present them in the most natural way; this is why the paper chose Haskell. We could implement the same in any Turing-complete imperative language, but then the code would swell by orders of magnitude.
I think you are still making an unfair generalization from this post. What you are saying is like reading a machine learning paper which has python examples and complaining that software development with python demands understanding advanced linear algebra.
For anyone confused here, the “simple” here comes from the simply-typed lambda calculus, that it models. This post addresses several issues with a tutorial paper on a dependently-typed lambda calculus, which is what all the build-up is for.
I would have found this blog post helpful when I was implementing the original tutorial paper, because I got stuck with the higher-order abstract syntax for lambdas. The original uses lambda literals from Haskell, which I couldn't figure it out how to express in Coq or Rust, because of the type recursion and some other issues. Whereas, I would easily be able to implement the first-order alternative presented here in either language.
> Church’s type theory is a formulation of type theory that was introduced by Alonzo Church in Church 1940. In certain respects, it is simpler and more general than the type theory introduced by Bertrand Russell in Russell 1908 and Whitehead & Russell 1927a. Since properties and relations can be regarded as functions from entities to truth values, the concept of a function is taken as primitive in Church’s type theory, and the λ-notation which Church introduced in Church 1932 and Church 1941 is incorporated into the formal language.
The "simple" from the title I wrote as the usual meaning of "simple" in English. I had some hard time devising a proper title, so I understand the complaints.
We distinguish two kinds of variables: Bound variables and
Free ones. The first kind of variables is called De Bruijn
indices: each bound variable is a natural number (starting
from zero) that designates the number of binders between
itself and a corresponding binder. For example, the term \x -
> \y -> x (the “K combinator”) is represented as \_ -> \_ -> 1.
(If we were returning y instead of x, we would write 0
instead.)
The footnote says:
Contrary to a De Bruijn index, a De Bruijn level is a natural
number indicating the number of binders between the
variable’s binder and the term’s root. For example, the term
\x -> \y -> x is represented as \_ -> \_ -> 0, where 0 is the
De Bruijn level of x. The De Bruijn level of y would be 1 if
we used it instead of x.↩
That doesn't look contradictory. An expression is a (syntax) tree, and every variable use has a unique path from the root to that use. This path crosses some sequence of binders, which we can label with integers.
If you assign integers from the inside out, as DB indices do, then the `x` usage in `\x -> \y -> x` passes one binder (`\y`) before landing on the correct one (`\x`), yielding `\_ -> \_ -> 1`.
If you assign integers from the outside in, as DB levels do, then the `x` usage lands on `\x` instantly, yielding `\_ -> \_ -> 0`.
De Bruijn came up with both systems, and it can be confusing to keep track of which one is which; but they are different systems.
I would have said, "that LOOKS contradictory but isnt"
because one is index and the other is a level but notationally they refer to the same syntactic construct, and therefore an assertion of value differs by intent. Index 1, level 0, Same syntax to represent.
To me, it "looks" contradictory. It has to be explained by word not by statement in notation.
If you combine these two naming schemes in the same syntax, of course it will be ambiguous. In the examples of the K combinator, they don't clash with each other though, as those are different examples.
This looks nice. Looking forward to going through it and the related earlier stuff carefully at leisure.
I'm sure the author is well aware, but Lennart Augustsson wrote a really nice blog post responding to the original "Simply Easy!" in 2007 that was a lot more fun and simple than the "Simply Easy" paper.
It's a constructor defined with infix syntax. You can make constructors with custom infix names by starting the name with the : character. Alternatively, you could call that constructor App or something and have the same effect:
data ITerm
= Ann CTerm Type
| Bound Int
| Free Name
| App ITerm CTerm
deriving (Show, Eq)
It defines a new infix data constructor. So if `it` and `ct` are values of type `ITerm` and `CTerm` respectively, `it :@: ct` is a value of type `ITerm`. (It could have been written using a prefix operator like `ITerm`'s other data constructors.)
That's a compact data structure, but now show us the type checker and the evaluator?
Your data structure is also not the simplest choice of syntax for lambda calculus, since you require an explicit type annotation on every function variable. I don't think a user of your implementation would find it "simple" to write even the identity function for a non-trivial type.
The typechecker and evaluator for this AST would be super simple.
If you want a simple typechecker then you need type annotations. If you want to have type inference then you either need to implement unification or go the bidir route (which still requires top level annotations). You can't have it both ways.
I'm sure the typechecker is as simple as you suggest for GP's language; but not showing it at all makes for an unfair comparison with the article. But the evaluator? Without out the trick of notation that is [x/y] substitution? It's not simple!
You are right that the typechecker gets significantly more complicated if type annotations are optional. But the article and the paper are about real implementations of the language, not arm-chair ones where the burden of type annotations isn't important.
I have to admit that I am out of my field, so help me a bit, you expressed that it must be dependently typed because false and true are a -> b -> a|b under union (and a->b->b and a->b->a respectively) so the the abstractions can take any functions subtyping a->b->a|b, thus to make them correct you need dependent types to verify that the abstractions take only True and False?
The only types available to you in this flavor of STLC are bool, bool -> bool, bool -> bool -> bool, (bool -> bool) -> bool, etc.
Structurally, if `true := \x\y.x`, the simplest attempt at typing it would be `true : bool -> bool -> bool`. But that means `true` can't have type `bool`!
What you need is to say that true (like false) chooses one of its two inputs to return, no matter what type that happens to be. So we introduce a type parameter (think Java generics, if that's what you're familiar with).
"Given any type T, `true T` has type T -> T -> T". A formalized notation for this (there is more than one notation you'll see) is `true : ∀ (T : Type), T -> T -> T`. And `false` has the same type. This type obviates the need for a declared `bool` type.
I don't believe the original performs NbE. It _looks_ like NbE, but the composition of `eval` and `quote` will not give you beta-normal forms. `quote` explicitly wraps inferrable terms in `Inf`, while `eval` eliminates `Inf`.
The author criticizes some design choices made by the paper's authors as not being simple enough. However, in fairness to that paper, it's aiming for dependently typed lambda calculus and, for reasons of continuity of exposition, is probably making sub-optimal choices up front that pay off later. The distinction between inferable and checkable types, for example, doesn't really pay off until you need to do beta-reduction in the type checker. The author of the present article has the luxury of stopping early, with just an STLC implementation.
I don't kind of agree with your statement, since I earlier implemented a 80-line dependent lambda calculus [1]. I think dependent types make type checking a bit more involved due to non-trivial type equality, but that's all about it.
The lambda calculus is simple. It consists of only four essential things, and with those four things we can compute anything that is computable. (I don't claim that the lambda calculus is simple to understand — certainly there are people who have a hard time grasping it. But that's a different issue.)
What the author is doing is not "the lambda calculus"; it's an extended lambda calculus for dependent types. That's a huge step in terms of complexity. Yes, it might be the simplest lambda calculus for the task (I didn't check), but that is not at all "how to keep lambda calculus simple". Just a very odd choice for a title, in my opinion.