[Haskell-cafe] Type-Level Programming

[Liam O'Connor]

I prefer Agda to Epigram, but different strokes for different folks.


In agda, you could define a list indexed by its size like this:

data Vec  : (A : Set) →  ℕ → Set where
 []  : Vec A 0
 _∷_ : ∀ {n : ℕ} → A → Vec A n → Vec A (1 + n)

So, we have a Vec data type, and on the type level it is a function
from some type A (which itself is of type Set) and a natural number
(the length) to a new type (of type Set).

The empty list is defined as a zero length vector, and cons therefore
increases the type-level length of the vector by one. Using this
method, Agda can be used to make a fully safe "head" implementation
that is statically verified not to crash:

head : ∀ { A : Set } { n : ℕ} → Vec A (1 + n) → A
head (x :: xs) = x

This uses the type system to ensure that the vector includes at least
one element.

Note that a similar thing can be achieved in Haskell with the right
extensions, however type-level naturals must be used:

data S n
data Z

data Vec a :: * -> * where
  Empty :: Vec a 0
  Cons   :: a -> Vec a b -> Vec a (S b)


safeHead  :: forall b. Vec a (S b) -> a
safeHead (Cons x xs) = x

(note: not tested)

The main difference here between Haskell and Agda is that the types
themselves are typed, and that the types contain real naturals not
fake ones like in Haskell


Cheers.
~Liam



On 26 June 2010 22:04, Andrew Coppin <andrewcoppin at btinternet.com> wrote:
> Tony Morris wrote:
>>
>> http://www.cs.nott.ac.uk/~txa/publ/ydtm.pdf
>>
>
> Ah yes, it was definitely Epigram I looked at. The intro to this looked
> promising, but by about 3 pages in, I had absolutely no clue what on Earth
> the text is talking about...
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>