4 ms·

I thought some like t ::= x (variable) | \x:T,t (abstraction) | t t

by a1o 3y ago

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.
cvoss 3y 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.
- solomonb 3y 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.
  - cvoss 3y ago
    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 3y ago
      Thats fair. I'm not GP but I do tend to agree that the AST used in that paper is overly complicated. Here is an STLC with bidir example which I believe to be easier to understand: https://github.com/solomon-b/lambda-calculus-hs/blob/main/main/01-BidirectionalTypechecking.hs https://github.com/solomon-b/lambda-calculus-hs/blob/main/ma...

by a1o 3y ago

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.

cvoss 3y 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.

solomonb 3y 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.
- cvoss 3y ago
  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 3y ago
    Thats fair. I'm not GP but I do tend to agree that the AST used in that paper is overly complicated. Here is an STLC with bidir example which I believe to be easier to understand: https://github.com/solomon-b/lambda-calculus-hs/blob/main/main/01-BidirectionalTypechecking.hs https://github.com/solomon-b/lambda-calculus-hs/blob/main/ma...