Suggestion: let expressions

[takanuva]

I'd like to suggest a small tweak to help writing code. The default application rule for pure type systems is as follow:

 L |- f: \/(x: A).B        L |- a: A
-------------------------------------
         L |- (f a): B[a/x]

I.e., both the function abstraction and the parameter have to be typeable on their own. My suggestion is to allow a let-expression within the language, with the following rule:

 L |- a: A        L |- b[a/x]: B
---------------------------------
      (let x = a in b): B

I.e., it first typechecks the "parameter", then beta-reduces the body, and only then checks the body of our "function". This extension keeps the calculus of constructions consistent, but makes it a bit more expressive, and it would allow to do things that now require Morte to load the expression from another file.

To avoid adding keywords, I'd suggest square brackets for Morte's syntax for that. E.g.,

[Nat = \/(N: *).\/(Z: N).\/(S: N -> N).N]
\(n: Nat) ->
n

And it would work as if we had a file ./Nat with that definition. What do you think?

[Gabriella439]

I will probably keep Morte as is in order to keep the spirit of being a true calculus of constructions implementation, but note that Dhall (which descends from Morte) has exactly the rule you requested:

https://github.com/dhall-lang/dhall-lang/blob/master/standard/semantics.md#let-expressions-1

The equivalent Dhall program would be:

let Nat = ∀(N : Type) → ∀(Z : N) → ∀(S : N → N) → N

in λ(n : Nat) → n

[takanuva]

IIRC, there are formalizations of pure type systems (and of course of CoC) which do have the let rule as well, which might be considered as a common extension (similar to the eta reduction).

[Gabriella439]

Hmm, alright, then. Would it be alright to use the same let/in syntax as Dhall?

[takanuva]

I think so. If you're ok with that, I can make a pull request for that feature. But that's just a suggestion, it's your call. :smile:

[Gabriella439]

Yeah, go for it! :)