How to keep lambda calculus simple

https://hirrolot.github.io/posts/how-to-keep-lambda-calculus-simple.html

by azhenley • 3 years ago

107 33 3 years ago

hirrolot.github.io

seanpquig2• 3 years ago

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.

solomonb6• 3 years ago

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.

It also doesn't mention any category theory...

seanpquig2• 3 years ago

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.

DonaldPShimoda• 3 years ago

I think the author's title is kind of misleading.

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.

solomonb6• 3 years ago

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.

dunham• 3 years ago

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:

https://github.com/idris-lang/Idris2/blob/main/libs/papers/L...

klysm• 3 years ago

For certain definitions of simple. I don’t think it’s a particular useful word because you can use it to justify almost anything.

a1o• 3 years ago

I thought some like

      t ::= x                         (variable)
           | \x:T,t                    (abstraction)
           | t t                       (application)
           | true                      (constant true)
           | false                     (constant false)
           | if t then t else t        (conditional)

Was simpler.

PartiallyTyped2• 3 years ago

If you define true and false as abstractions:

    true ::= \x\y,x
    false ::= \x\y,y

Then the conditional comes for free, since it is an application of true. You can define not as

    not ::= \b, b false true

You can then define 'and' as

    and ::= \x\y, x y false

cvoss5• 3 years ago

That won't work in simply typed lambda calculus. (Try to write down the types involved!) Either untyped or dependently typed is required.

cvoss5• 3 years ago

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.

solomonb6• 3 years ago

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.

thaliaarchi• 3 years ago

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.

cubefox• 3 years ago

More on "simple":

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.

https://plato.stanford.edu/entries/type-theory-church/

Hirrolot5• 3 years ago

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.

solomonb6• 3 years ago

This article is odd. The author seems to imply they are introducing NBE in their second redesign, but the original paper performs NBE as well.

Hirrolot5• 3 years ago

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`.

cvoss5• 3 years ago

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.

Hirrolot5• 3 years ago

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.

[1] https://gist.github.com/Hirrolot/27e6b02a051df333811a23b97c3...

tempodox• 3 years ago

What the hell is `:@:`? Cannot google that, and the GHC docs don't tell either.

joek1301• 3 years ago

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.)

tikhonj• 3 years ago

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)

ggm2• 3 years ago

The body says:

  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.↩

Twisol• 3 years ago

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.

ggm2• 3 years ago

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.

mafm• 3 years ago

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.

http://augustss.blogspot.com/2007/10/simpler-easier-in-recen...

How to keep lambda calculus simple

Related Stories