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@btinternet.com> wrote:
Tony Morris wrote:
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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe