[HN Gopher] How to Keep Lambda Calculus Simple
___________________________________________________________________
How to Keep Lambda Calculus Simple
Author : azhenley
Score : 59 points
Date : 2023-07-08 15:32 UTC (7 hours ago)
(HTM) web link (hirrolot.github.io)
(TXT) w3m dump (hirrolot.github.io)
| DonaldPShimoda wrote:
| 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 wrote:
| 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 wrote:
| 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...
| ggm wrote:
| 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.-
| seanpquig wrote:
| 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.
| solomonb wrote:
| 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...
| [deleted]
| cvoss wrote:
| 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.
| tempodox wrote:
| What the hell is `:@:`? Cannot google that, and the GHC docs
| don't tell either.
| joek1301 wrote:
| 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 wrote:
| 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)
| thaliaarchi wrote:
| 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 wrote:
| 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
| l-notation which Church introduced in Church 1932 and Church
| 1941 is incorporated into the formal language.
|
| https://plato.stanford.edu/entries/type-theory-church/
| klysm wrote:
| 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 wrote:
| 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]
| PartiallyTyped wrote:
| 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 wrote:
| That won't work in simply typed lambda calculus. (Try to
| write down the types involved!) Either untyped or dependently
| typed is required.
| PartiallyTyped wrote:
| 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 wrote:
| 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.
| cvoss wrote:
| 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.
| solomonb wrote:
| 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.
| cvoss wrote:
| 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.
| solomonb wrote:
| 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.
___________________________________________________________________
(page generated 2023-07-08 23:00 UTC)