Lists with type-encoded length

LList.hs

{-# LANGUAGE DataKinds, GADTs, KindSignatures, TemplateHaskell #-}

-- | Lists with type-encoded length
--
-- Includes TH macros for concise usage of Peano naturals at type and term
-- level.
--
-- Examples:
--
-- >>> :t Nil
-- Nil :: LList 'Z a
--
-- >>> :t Cons () Nil
-- Cons () Nil :: LList ('S 'Z) ()
--
-- >>> head $ Cons () Nil
-- ()
--
-- >>> head Nil
-- Couldn't match type 'Z with 'S n0 ...
--
-- >>> head $ replicate $(singNat 20) ()
-- ()
module Data.LList (
                  -- * Peano naturals
                    Nat (..)
                  , NatSing (..)

                  -- * LList type
                  , LList (..)

                  -- * Type-safe utility functions
                  , head
                  , replicate

                  -- * Convenience macros
                  , typeNat
                  , termNat
                  , singNat
                  ) where

import Prelude hiding (head, replicate)

import Language.Haskell.TH

data Nat = Z | S Nat

-- | Peano singletons
data NatSing (n :: Nat) where ZS :: NatSing Z
                              SS :: NatSing n -> NatSing (S n)

data LList (len :: Nat) a where Nil :: LList Z a
                                Cons :: a -> LList len a -> LList (S len) a

-- | Safe head function
--
-- Calling this on an empty list is a type error.
head :: LList (S n) a -> a
head (Cons x _) = x

-- | Like 'Prelude.replicate'
replicate :: NatSing n -- ^ Length as a singleton
          -> a -- ^ Element to replicate
          -> LList n a
replicate ZS _ = Nil
replicate (SS n) x = Cons x $ replicate n x

-- | Macro for generating Peano types
typeNat :: Int -> Q Type
typeNat = natMacro AppT PromotedT 'S 'Z

-- | Macro for generating Peano terms
termNat :: Int -> Q Exp
termNat = natMacro AppE ConE 'S 'Z

-- | Macro for generating Peano singletons
singNat :: Int -> Q Exp
singNat = natMacro AppE ConE 'SS 'ZS

natMacro :: (e -> e -> e) -> (Name -> e) -> Name -> Name -> Int -> Q e
natMacro app con s z n = return $ iterate (app $ con s) (con z) !! n