<p>The representation issue of W-types was resolved by <a href="https://jashug.github.io/papers/whynotw.pdf" rel="noreferrer">Jasper Hugunin</a>. So from type formers <span class="math-container">$0$</span>, <span class="math-container">$1$</span>, <span class="math-container">$2$</span>, <span class="math-container">$W$</span>, <span class="math-container">$\Pi$</span>, <span class="math-container">$\Sigma$</span>, identity and a universe hierarchy we do get all indexed inductive families with exactly the expected elimination rules and definitional computation rules.</p>
<p>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.</p>

CC BY-SA 4.0
2024-01-31T14:59:21.183Z
I wonder if it would be sufficient to just add CTT's Path types or HoTT's interval so that function extensionality can be proven with computational content. I might give that a try.

I'm reading Jasper Hugunin's paper now as well.
Jake
CC BY-SA 4.0
2024-02-01T04:58:02.090Z
This is quite a nice answer. I'm going to play around with this, and adding one of a couple different computational mechanisms for function extensionallity and see which one I like better. Having function extensionallity is a nice property of the system. I'll compare the proofs and reductions and see if I like the canonical predicate or this better.

Thanks!
Jake
CC BY-SA 4.0
2024-01-31T13:41:51.473Z
2024-01-31T13:47:22.427Z
2024-01-31T13:47:22.427Z
András Kovács
<p>You could start with <a href="https://github.com/andrejbauer/spartan-type-theory" rel="nofollow noreferrer">Spartan type theory</a> (which honestly should be upgraded to use evaluation-by-normalization) and add simple inductive datatypes to them. This would involve several steps.</p>
<p>First, add inductive datatype definitions of the form</p>
<pre><code>data T = C1 of T1 | ⋯ | Cn of Tn
</code></pre>
<p>where <code>Ci</code> are constructor names and <code>Ti</code> are types they carry. Examples:</p>
<pre><code>data Bool = True of Unit | False of Unit
data Nat = Zero of Unit | Succ of Nat
data BoolList = Nil | Cons of Bool × BoolList
</code></pre>
<p>Then you need to implement an elimination form, for instance as a <code>match</code> statement with shallow patterns:</p>
<pre><code>match e with
| C1 x1 =&gt; e1
...
| Cn xn =&gt; en
end
</code></pre>
<p>where <code>C1</code>, ..., <code>Cn</code> are precisely all constructors of one of previously defined datatypes.</p>
<p>Type-checking of constructors is easy. Type-checking of <code>match</code> can be tricky, it's best if in the first attempt you make it simply-typed, i.e., all branches of <code>match</code> return the exact same type.</p>
<p>From here there are many possible generalizations:</p>
<ol>
<li>Allow type parameters, e.g. <code>List t</code> for arbitrary <code>t</code> instead of <code>BoolLIst</code>, <code>IntList</code>, ...</li>
<li>Allow mutually recursive datatypes.</li>
<li>Dependently-typed <code>match</code>.</li>
<li>Dependently typed constructors in inductive datatypes.</li>
</ol>
<p>I do not know of a good instructional imlplementation of such datatypes. A student of mine extended <a href="http://plzoo.andrej.com" rel="nofollow noreferrer">PL Zoo</a> MiniHaskell with inductive datatypes, you may rummage through <a href="https://github.com/BaSO-4/plzoo/tree/master/src/minihaskell" rel="nofollow noreferrer">his branch of MiniHaskell</a> and compare it to the <a href="https://github.com/andrejbauer/plzoo/tree/master/src/minihaskell" rel="nofollow noreferrer">original</a> to see what changed.</p>

CC BY-SA 4.0
2024-01-31T08:22:53.087Z
2024-01-31T08:22:53.087Z
Andrej Bauer
<p>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 &quot;synthetic&quot; nature of HoTT/MLTT for this. The exact properties of the system do not matter much beyond that.</p>
<p>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...</p>
<p>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 <a href="https://mazzo.li/epilogue/index.html%3Fp=324.html" rel="nofollow noreferrer">such as their lack of canonical representation</a> 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 &quot;oomf&quot; 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.</p>
<p>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?</p>

<type-theory><dependent-type><type-systems><typed-lambda-calculus><homotopy-type-theory>
Generalizations, or extensions of W-types in MLTT
Jake
# Generalizations, or extensions of W-types in MLTT

(Asked by: username_0 on 2024-01-31)

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](https://mazzo.li/epilogue/index.html%3Fp=324.html) 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?

**Tags:** type-theory, dependent-type, type-systems, typed-lambda-calculus, homotopy-type-theory


---

## 2 answers

### Answer by username_1 on 2024-01-31. Score: 6 | Accepted answer

The representation issue of W-types was resolved by [Jasper Hugunin](https://jashug.github.io/papers/whynotw.pdf). 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.

> **Comments:**
> **username_0**: I wonder if it would be sufficient to just add CTT's Path types or HoTT's interval so that function extensionality can be proven with computational content. I might give that a try.  I'm reading Jasper Hugunin's paper now as well.  
> **username_0**: This is quite a nice answer. I'm going to play around with this, and adding one of a couple different computational mechanisms for function extensionallity and see which one I like better. Having function extensionallity is a nice property of the system. I'll compare the proofs and reductions and see if I like the canonical predicate or this better.  Thanks!  

---

### Answer by username_2 on 2024-01-31. Score: 3

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:

Allow type parameters, e.g. List t for arbitrary t instead of BoolLIst, IntList, ...
Allow mutually recursive datatypes.
Dependently-typed match.
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.


---

