It's annoying that for every new construct I add to my language, I need to add the type former, the introduction form, the elimination form, and typing rules for all of these
If only there were some generalized way of defining all of these once and for all

I gotta say, though, defining a lot of small rules is a lot more digestible than defining one gigantic frankenrule for case expressions


Uh oh. I just realized I can get non-prenex size abstractions just by wrapping polymorphic sized types in pairs

f: (∀α. τ1) → τ2
f': (∀α. τ1) × ⊤ → τ2

I need pairs to be able to hold size-abstracted functions though because closure-conversion wraps around let-bound possibly sized-abstracted functions. I only meant for prenex sized types to simplify typing so hopefully this doesn't cause any real trouble
I mean Agda basically treats Size like its own special size, so if they can do that, surely I can do this

fix natleast (n: ℕ [∞]): ∀α. Type :=
match n with
| zero => Λα. ℕ [α]
| succ m => Λα. (natleast m) [α+1]

You can specify a Nat type whose size is at least n. Don't like that

I lied
Look at this

eqsz: forall a, b. (f: forall a. Type) -> Type
eqsz [a] [b] f = f [a] == f [b]

size equality

reflsz: forall a. (f: forall a. Type) -> eqsz [a] [a] f
reflsz [a] f = refl (f [a])

I didn't really have a point to make, but

Sign in to participate in the conversation

A Mastodon instance for users who like the study of programming languages, formal semantics, types, or linguistics.