List.hs

{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE UndecidableInstances   #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE DeriveDataTypeable     #-}
{-# LANGUAGE EmptyDataDecls         #-}

{-# LANGUAGE Rank2Types      #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE KindSignatures  #-}
-- | Heterogenous list in the spirit of Oleg Kiselyov's List
module TypeLevel.List (
    Nil
  , (:::)
  , tyListHead
  , tyListTail
  , TyFold(..)
  ) where

import Data.Functor    ((<$>))
import Data.Typeable --   (Typeable(..))
import GHC.Prim        (Constraint)

import TypeLevel.TypeEq
import TypeLevel.Proxy



----------------------------------------------------------------
-- Data type
----------------------------------------------------------------

-- | Sets are represented as linked lists
data Nil      deriving Typeable
data a ::: b  deriving Typeable
infixr 5 :::

tyListHead :: (a ::: b) -> a
tyListHead _ = undefined

tyListTail :: (a ::: b) -> b
tyListTail _ = undefined


instance Show Nil where
  show _ = ""
instance Typeable a => Show (a ::: Nil) where
  show = show . typeOf . tyListHead
instance (Typeable a, Show (b ::: c)) => Show (a ::: b ::: c) where
  show x = show (typeOf $ tyListHead x) ++ " ::: " ++ show (tyListTail x)



----------------------------------------------------------------
-- Fold
----------------------------------------------------------------

-- | Fold over type list
class TyFold (pred :: * -> Constraint) xs where
  tyFoldr
    :: Proxy pred
       -- ^ Carry around proxy for constraint
    -> (forall t . pred t => Proxy t -> a -> a)
       -- ^ Fold function
    -> a
       -- ^ Initial value
    -> Proxy xs
       -- ^ Type level list
    -> a

instance (pred t, TyFold pred xs) => TyFold pred (t ::: xs) where
  tyFoldr pred f x0 list
    = f (tyListHead <$> list)
    $ tyFoldr pred f x0 (tyListTail <$> list)

instance TyFold pred Nil where
  tyFoldr _ _ x _ = x

Proxy.hs

{-# LANGUAGE PolyKinds #-}
-- | Proxy types
module TypeLevel.Proxy ( 
    Proxy(..)
  , proxy
  , unproxy
  ) where

-- | Proxy data type 
data Proxy t = Proxy 

proxy :: t -> Proxy t
proxy _ = Proxy

unproxy :: Proxy t -> t
unproxy _ = undefined

instance Functor Proxy where
  fmap _ _ = Proxy