Expending ProosTT
This issue is meant to be a place for discussing the future works on the type-checker.
The current TT implemented doesn't have any "complex" types and terms, a first step would be to implement natural numbers. This already gives rise to a major problem : because of the lack of universe polymorphism, it is not possible in our current TT to add a universal eliminator (read, recursor) on this inductive type, unless we'd generate a different induction principle for each type universe. For example, encoding something like :
def foo : Nat -> Type 1
| 0 => Type 0
| n.succ => Type 0 -> foo n
would not be possible in the current ProosTT. In other proof-assistant supporting universe-polymorphism, this wouldn't be an issue. the eliminator would be parametrized by a universe. For example, Lean's nat eliminator is typed as :
Nat.rec.{u} : (motive : Nat → Sort u) → motive Nat.zero → ((n : Nat) → motive n → motive (Nat.succ n)) → (t : Nat) → motive t
There are a few possible solutions to this problem. One would be to add universe polymorphism, the other would be to generate universe-specific eliminators "on the fly", though I do not know how well this would work.
I don't think adding universe polymorphism would be too difficult. Knowing the work on unification hasn't yet started, it would not pose as a great challenge to add it. Furthermore, the unification of universes and terms can be made separately, so we could work with having explicit polymorphism for out universe polymorphic functions. for example, our nat recursors would now be :
nat_rec_p : (P : Nat → Prop) → P Z → ((n : Nat) → P n → P (S n)) → (t : Nat) → P t
nat_rec_t@{i} : (P : Nat → Type(i)) → P Z → ((n : Nat) → P n → P (S n)) → (t : Nat) → P t
How do you guys feel about this ?
Additionally, what should we be working on first for the type-checker ? Should we first focus on unification or the addition or new types like equality and Nats ? These types' recursors could be hardcoded for Prop and Type(0) until universe polymorphism gets implemented. Additionally, unification seems to me like a quite big thing to tackle and would, in my opinion, need some consideration before diving into it. I started coding the type-checker before thinking things through last time, and it led to lengthy process of bug-fixing and verification, and I'd like to make sure everything is planned out before starting the work on unification.