A list type with statically determined length encoded in its type

LList.hs

{-# LANGUAGE DataKinds
           , GADTs
           , KindSignatures
           , StandaloneDeriving
           , TypeOperators
           #-}

-- | A list type with statically determined length encoded in its type
--
-- Requires GHC 7.6.1 or greater.
module LList where

import Prelude hiding (foldr)

import Data.Foldable

import GHC.TypeLits

data LList (len :: Nat) a where LNil :: LList 0 a
                                (:::) :: a -> LList n a -> LList (n + 1) a
infixr 5 :::

deriving instance Show a => Show (LList len a)

instance Functor (LList len) where fmap f LNil = LNil
                                   fmap f (x ::: xs) = f x ::: fmap f xs

instance Foldable (LList len) where
    foldr _ init LNil = init
    foldr f init (x ::: xs) = foldr f (f x init) xs