⌨️ Add `deftype`

[TOTBWF]

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.

[jonsterling]

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?

[TOTBWF]

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 𝕀!

[jonsterling]

What I meant was, can I have an example of how your proposed deftype helps with this?

[TOTBWF]

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.

[jonsterling]

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.