Generalizations, or extensions of W-types in MLTT

Question

I'm interested in making a very stripped down implementation of MLTT, or possibly HoTT or cubical type theory (though I've yet to grok the glue rule in cubical type theory and both it and composition look a bit hard to implement). I'm primarily interested in having a system where interesting things can be proven by relatively small proofs and hope to leverage the "synthetic" nature of HoTT/MLTT for this. The exact properties of the system do not matter much beyond that.

I want this very stripped down implementation to still be able to prove useful things so I of course need to add the typical induction principals and types for things like products, co-products, natural numbers, etc...

That's probably enough to get very far with this system but I'd prefer to have something like W-types that give me induction principals for many things boot strapped from only a bottom, top, and 2 element type. Still W-types have issues such as their lack of canonical representation and they can't represent things like inductive recursive types as far as I'm aware. In particular I was kind of hoping to be able to represent logical relations which seems to require some extra "oomf" than W-types provide. Still I'm very willing forgo this, there are other areas of math that I'd be happy to explore with this system that do not need logical relations.

Are there any systems that have something like a generalization of W-types? Is there perhaps something like W-types that solves the canonical representation issue without resorting to extensional equality?

Answer 1

The representation issue of W-types was resolved by Jasper Hugunin. So from type formers $0$, $1$, $2$, $W$, $\Pi$, $\Sigma$, identity and a universe hierarchy we do get all indexed inductive families with exactly the expected elimination rules and definitional computation rules.

Logical relation arguments should be definable in this setup. We don't get inductive-recursive types, but they are rarely needed in logical relations (I don't know any instances). Also, many apparently IR definitions can be rephrased using large inductive types.

Answer 2

You could start with Spartan type theory (which honestly should be upgraded to use evaluation-by-normalization) and add simple inductive datatypes to them. This would involve several steps.

First, add inductive datatype definitions of the form

data T = C1 of T1 | ⋯ | Cn of Tn

where Ci are constructor names and Ti are types they carry. Examples:

data Bool = True of Unit | False of Unit
data Nat = Zero of Unit | Succ of Nat
data BoolList = Nil | Cons of Bool × BoolList

Then you need to implement an elimination form, for instance as a match statement with shallow patterns:

match e with
| C1 x1 => e1
...
| Cn xn => en
end

where C1, ..., Cn are precisely all constructors of one of previously defined datatypes.

Type-checking of constructors is easy. Type-checking of match can be tricky, it's best if in the first attempt you make it simply-typed, i.e., all branches of match return the exact same type.

From here there are many possible generalizations:

1. Allow type parameters, e.g. List t for arbitrary t instead of BoolLIst, IntList, ...
2. Allow mutually recursive datatypes.
3. Dependently-typed match.
4. Dependently typed constructors in inductive datatypes.

I do not know of a good instructional imlplementation of such datatypes. A student of mine extended PL Zoo MiniHaskell with inductive datatypes, you may rummage through his branch of MiniHaskell and compare it to the original to see what changed.