-
Notifications
You must be signed in to change notification settings - Fork 25
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Suggestion: let expressions #73
Comments
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 |
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). |
Hmm, alright, then. Would it be alright to use the same |
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. 😄 |
Yeah, go for it! :) |
I'd like to suggest a small tweak to help writing code. The default application rule for pure type systems is as follow:
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:
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.,
And it would work as if we had a file
./Nat
with that definition. What do you think?The text was updated successfully, but these errors were encountered: