[<<][haskell][>>][..]
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:

https://www.parsonsmatt.org/2017/04/26/basic_type_level_programming_in_haskell.html

Notes:

- 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
  types.

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


Read that a bit more, then graduate to this:

https://www.schoolofhaskell.com/user/konn/prove-your-haskell-for-great-safety/dependent-types-in-haskell




[Reply][About]
[<<][haskell][>>][..]