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) → τ2f': (∀α. τ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

``(λx: (∀α. τ) × ⊤. e)``

ew

``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

It's okay. I'll think about it in June

I lied
Look at this

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

size equality

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

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

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