exports
  listHasLength
  listSequence
  listFunctor
  listMonoid
  head
  tail

import Monoid

implicit listHasLength : HasLength List = rec
  .length
    Cons _ xs = 1 + length xs
    Nil       = 0

implicit listSequence : Sequence List = rec
  .toList   = id
  .fromList = id

implicit listFunctor : Functor List = rec
  .map
    f (Cons x xs) = Cons (f x) xs
    _ Nil         = Nil

implicit listMonoid : Monoid List = rec
  .empty = []
  .append
    Nil         ys = ys
    (Cons x xs) ys = Cons x (append xs ys)

head : List a -> a
  x :: _ = x
  Nil    = error "head: empty list"

tail : List a -> List a
  _ :: xs = xs
  Nil     = error "tail: empty list"