5

The following explanation lacks mathematicial precision but should explain what is going on. A GADT is a special case of a recursive type. A recursive type $T$ is a solution of a type equation of the form $$T = \Phi(T).$$ (If this is not clear, please ask.) Sometimes $\Phi$ depends on a parameter $p : P$ of some given type $P$, so we have a parameterized ...


3

Yes and no. The obvious difference is that indexed types are able to vary in the result type of each constructor. So you can do: data T : ℕ → Set where t : T 5 You can do this with a parameterized type by taking an argument: data T (n : ℕ) : Set where t : n ≡ 5 → T n But ≡ is itself an indexed type, so you need something indexed at the bottom (≡ can ...


1

I'm uncertain what you're referring to exactly, but I can remark on a few things. The first is that the usual problem with W-types is that encoding inductive types with them does not necessarily give you the right induction principles. For instance, we can try to define the natural numbers like so: F : 2 → Type F 0 = ⊥ F 1 = ⊤ ℕ : Type ℕ = W 2 F zero : ℕ ...


Only top voted, non community-wiki answers of a minimum length are eligible