Liam O'Connor liamoc at cse.unsw.edu.au
Sat Jun 26 08:59:19 EDT 2010

```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

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