cooltt
cooltt copied to clipboard
RedPRL
⌨️ Add `deftype`
Motivation
Currently, the only way to define types is via def foo : type := ..., which has some interesting ramifications regarding fibrancy. In particular, we can't define record types with fields of type I -> A, and instead have to resort to some weird hacks like ext i => A with [], which I think we can all agree is suboptimal. We should probably think about adding a way of defining honest-to-god types, rather than only codes.
Proposal
The proposed syntax is as follows
deftype <typename> <cells> := <definition>
The cells would then desugar to a pi type.
We can just inline these during elaboration to avoid having to change the core, but perhaps there's some value in adding these to the core with some unfolding rules.
Hmm, I don't yet see why deftype addresses the way that we can't have records with fields of type I->A. Can you an example?
Consider
def example : type :=
sig (p : 𝕀 → ℕ)
This will elaborate to a code, which will then require all of the fields of the CodeSignature to also be codes, but there's no code for 𝕀!
What I meant was, can I have an example of how your proposed deftype helps with this?
Sorry, misunderstood your request!
With deftype, we'd elaborate this as a Signature, which should allow us to elaborate the fields as types, which solves the problem.
Oh I see. I’m ok with it
On Jun 24, 2022, at 2:02 PM, Reed Mullanix @.***> wrote:
Sorry, misunderstood your request!
With deftype, we'd elaborate this as a Signature, which should allow us to elaborate the fields as types, which solves the problem.
— Reply to this email directly, view it on GitHub, or unsubscribe. You are receiving this because you commented.