Thu May 9 14:54:39 EDT 2019

Type level programming

I need to start from ground up, now that I sort of know what I want.
The first thing to do is to wrap Seq to have fixed size vectors.

Let's start here:



- Data Kinds are there to restrict kinds, e.g. avoid Succ :: * -> *,
  which would allow e.g. Succ Bool, allowing Succ :: Nat -> Nat

- GADTs allow to create parametric structures, where parameters can
  have constraints (e.g. be only one of a finite set of tupes).

- The combination of these two allows creation of type-level vectors

- Type Families then provide a mechanism to organize parameterized

- Then there's some notes about how this is hard to use

Read that a bit more, then graduate to this: