Open TOTBWF opened 2 years ago
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.
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 typeI -> A
, and instead have to resort to some weird hacks likeext 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
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.