module Data.Vector.Heterogenous.HList
(
HList (..)
, HLength (..)
, List2HList (..)
, HList2List (..)
, HTake1 (..)
, HDrop1 (..)
, ConstraintBox (..)
, Downcast (..)
, ShowBox (..)
, AnyBox (..)
, HCons (..)
, UnHList (..)
, HAppend
, Distribute (..)
, Replicate (..)
, Map (..)
, Reverse (..)
, (:!) (..)
, Index (..)
, (++) (..)
, ($) (..)
, Concat (..)
, Length (..)
, Length1 (..)
, Nat1(..)
, Nat1Box(..)
, ToNat1
, FromNat1
)
where
import Data.Monoid
import GHC.TypeLits
import Unsafe.Coerce
data HList :: [*] -> * where
HNil :: HList '[]
(:::) :: t -> HList ts -> HList (t ': ts)
infixr 5 :::
instance Show (HList '[]) where
show _ = "HNil"
instance (Show x, Show (HList xs)) => Show (HList (x ': xs)) where
show (x:::xs) = show x ++":::"++show xs
instance Eq (HList '[]) where
xs==ys = True
instance (Eq x, Eq (HList xs)) => Eq (HList (x ': xs)) where
(x:::xs)==(y:::ys) = (x==y)&&(xs==ys)
instance Ord (HList '[]) where
compare HNil HNil = EQ
instance (Ord x, Ord (HList xs)) => Ord (HList (x ': xs)) where
compare (x:::xs) (y:::ys) =
case compare x y of
EQ -> compare xs ys
LT -> LT
GT -> GT
instance Monoid (HList '[]) where
mempty = HNil
HNil `mappend` HNil = HNil
instance (Monoid x, Monoid (HList xs)) => Monoid (HList (x ': xs)) where
mempty = mempty:::mempty
(x:::xs) `mappend` (y:::ys) = (x `mappend` y):::(xs `mappend` ys)
class HLength xs where
hlength :: xs -> Int
instance HLength (HList '[]) where
hlength _ = 0
instance (HLength (HList xs)) => HLength (HList (x ': xs)) where
hlength (x:::xs) = 1+hlength xs
class HList2List xs a | xs -> a where
hlist2list :: xs -> [a]
instance HList2List (HList '[]) a where
hlist2list xs = []
instance (HList2List (HList xs) a) => HList2List (HList (a ':xs)) a where
hlist2list (x:::xs) = x:(hlist2list xs)
class List2HList x xs where
list2hlist :: [x] -> HList (x ': xs)
instance List2HList x '[] where
list2hlist [] = error "List2HList x HNil: cannot append empty list"
list2hlist (x:[]) = x:::HNil
list2hlist _ = error "List2HList x HNil: too many elements in list"
instance (List2HList x xs) => List2HList x (x ': xs) where
list2hlist [] = error "List2HList x HNil: cannot append empty list"
list2hlist (x:xs) = x:::(list2hlist xs)
class HDrop1 n xs1 xs2 | n xs1 -> xs2 where
hdrop1 :: n -> xs1 -> xs2
instance HDrop1 (Nat1Box Zero) (HList xs1) (HList xs1) where
hdrop1 n xs = xs
instance (HDrop1 (Nat1Box n) (HList xs1) (HList xs2)) =>
HDrop1 (Nat1Box (Succ n)) (HList (x ': xs1)) (HList xs2) where
hdrop1 _ (x:::xs) = hdrop1 (Nat1Box :: Nat1Box n) xs
class HTake1 n xs1 xs2 | n xs1 -> xs2 where
htake1 :: n -> xs1 -> xs2
instance HTake1 (Nat1Box Zero) (HList xs1) (HList '[]) where
htake1 _ _ = HNil
instance (HTake1 (Nat1Box n) (HList xs1) (HList xs2)) => HTake1 (Nat1Box (Succ n)) (HList (x ': xs1)) (HList (x ': xs2)) where
htake1 _ (x:::xs) = x:::(htake1 (Nat1Box :: Nat1Box n) xs)
class ConstraintBox box a where
box :: a -> box
unsafeUnbox :: box -> a
class Downcast h box where
downcast :: h -> [box]
downcastAs :: (a->box) -> h -> [box]
downcastAs box = downcast
instance Downcast (HList '[]) a where
downcast HNil = []
instance (ConstraintBox box x, Downcast (HList xs) box) => Downcast (HList (x ': xs)) box where
downcast (x:::xs) = (box x):(downcast xs)
data AnyBox = forall a. AnyBox !a
data ShowBox = forall a. (Show a) => ShowBox !a
instance Show ShowBox where
show (ShowBox a) = show a
instance (Show a) => ConstraintBox ShowBox a where
box a = ShowBox a
unsafeUnbox (ShowBox a) = unsafeCoerce a
type family HCons (x :: *) (xs :: *) :: *
type instance HCons x (HList xs) = HList (x ': xs)
type family UnHList (xs :: *) :: [a]
type instance UnHList (HList xs) = xs
type family HAppend xs ys :: *
type instance HAppend (HList xs) (HList ys) = HList (xs ++ ys)
type family Distribute (xs::[a->b]) (t::a) :: [b]
type instance Distribute '[] a = '[]
type instance Distribute (x ': xs) a = (x a) ': (Distribute xs a)
type family Replicate (n::Nat) (x::a) :: [a]
type instance Replicate n x = Replicate1 (ToNat1 n) x
type family Replicate1 (n::Nat1) (x::a) :: [a]
type instance Replicate1 Zero x = '[]
type instance Replicate1 (Succ n) x = x ': (Replicate1 n x)
type family Map (f :: a -> a) (xs::[a]) :: [a]
type instance Map f '[] = '[]
type instance Map f (x ': xs) = (f x) ': (Map f xs)
type family Length (xs :: [a]) :: Nat
type instance Length xs = FromNat1 ( Length1 xs )
type family Length1 (xs::[a]) :: Nat1
type instance Length1 '[] = Zero
type instance Length1 (x ': xs) = Succ (Length1 xs)
type family Reverse (xs::[a]) :: [a]
type instance Reverse '[] = '[]
type instance Reverse (x ': xs) = Reverse xs ++ '[x]
type family (:!) (xs::[a]) (i::Nat) :: a
type instance (:!) xs n = Index xs (ToNat1 n)
type family Index (xs::[a]) (i::Nat1) :: a
type instance Index (x ': xs) Zero = x
type instance Index (x ': xs) (Succ i) = Index xs i
type family ($) (f :: a -> b) (a :: a) :: b
type instance f $ a = f a
type family (xs :: [a]) ++ (ys :: [a]) :: [a]
type instance '[] ++ ys = ys
type instance (x ': xs) ++ ys = x ': (xs ++ ys)
type family Concat (xs :: [[a]]) :: [a]
type instance Concat '[] = '[]
type instance Concat (x ': xs) = x ++ Concat xs
type Take (n::Nat) (xs :: [*]) = Take1 (ToNat1 n) xs
type family Take1 (n::Nat1) (xs::[*]) :: [*]
type instance Take1 Zero xs = '[]
type instance Take1 (Succ n) (x ': xs) = x ': (Take1 n xs)
data Nat1 = Zero | Succ Nat1
data Nat1Box (n::Nat1) = Nat1Box
type family FromNat1 (n :: Nat1) :: Nat
type instance FromNat1 Zero = 0
type instance FromNat1 (Succ Zero) = 1
type instance FromNat1 (Succ (Succ Zero)) = 2
type instance FromNat1 (Succ (Succ (Succ Zero))) = 3
type instance FromNat1 (Succ (Succ (Succ (Succ Zero)))) = 4
type instance FromNat1 (Succ (Succ (Succ (Succ (Succ Zero))))) = 5
type instance FromNat1 (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))) = 6
type family ToNat1 (n :: Nat) :: Nat1
type instance ToNat1 0 = Zero
type instance ToNat1 1 = Succ (ToNat1 0)
type instance ToNat1 2 = Succ (ToNat1 1)
type instance ToNat1 3 = Succ (ToNat1 2)
type instance ToNat1 4 = Succ (ToNat1 3)
type instance ToNat1 5 = Succ (ToNat1 4)
type instance ToNat1 6 = Succ (ToNat1 5)
type instance ToNat1 7 = Succ (ToNat1 6)
type instance ToNat1 8 = Succ (ToNat1 7)
type instance ToNat1 9 = Succ (ToNat1 8)
type instance ToNat1 10 = Succ (ToNat1 9)
type instance ToNat1 11 = Succ (ToNat1 10)
type instance ToNat1 12 = Succ (ToNat1 11)
type instance ToNat1 13 = Succ (ToNat1 12)
type instance ToNat1 14 = Succ (ToNat1 13)
type instance ToNat1 15 = Succ (ToNat1 14)
type instance ToNat1 16 = Succ (ToNat1 15)
type instance ToNat1 17 = Succ (ToNat1 16)
type instance ToNat1 18 = Succ (ToNat1 17)
type instance ToNat1 19 = Succ (ToNat1 18)
type instance ToNat1 20 = Succ (ToNat1 19)