6 ms·

How to keep lambda calculus simple

• seanpquig 3y 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.
  • deleted 3y ago
    [deleted]
  • solomonb 3y 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...
    • seanpquig 3y 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.
      • solomonb 3y ago
        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.
      • Hirrolot 3y ago
        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.
• DonaldPShimoda 3y 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.
  • solomonb 3y 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 3y 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/Language/IntrinsicScoping/TypeTheory.idr https://github.com/idris-lang/Idris2/blob/main/libs/papers/L...
• klysm 3y 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 3y 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.
  • deleted 3y ago
    [deleted]
  • PartiallyTyped 3y 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
    • cvoss 3y ago
      That won't work in simply typed lambda calculus. (Try to write down the types involved!) Either untyped or dependently typed is required.
      • PartiallyTyped 3y ago
        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? Is this correct?
        • cvoss 3y ago
          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.
• thaliaarchi 3y 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 3y 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/ https://plato.stanford.edu/entries/type-theory-church/
  • Hirrolot 3y 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.
• solomonb 3y 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.
  • Hirrolot 3y 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`.
• cvoss 3y 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.
  • Hirrolot 3y 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/27e6b02a051df333811a23b97c375196 https://gist.github.com/Hirrolot/27e6b02a051df333811a23b97c3...
• tempodox 3y ago
  What the hell is `:@:`? Cannot google that, and the GHC docs don't tell either.
  • joek1301 3y 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 3y 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)
• ggm 3y 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 3y 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.
    • ggm 3y 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.
      • Hirrolot 3y ago
        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.
• mafm 3y 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-recent-paper-simply.html http://augustss.blogspot.com/2007/10/simpler-easier-in-recen...