{-# LANGUAGE CPP #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleContexts #-}
module Data.HList.HList
( HList(..)
, Append
, hAppend
, HInit(..)
) where
import Prelude hiding (reverse)
import Data.Kind (Type)
import Data.Monoid (Monoid, mappend, mempty)
import Data.Semigroup
import Data.Proxy
data HList :: [Type] -> Type where
HNil :: HList '[]
(:+:) :: x -> HList xs -> HList (x ': xs)
infixr 5 :+:
instance Show (HList '[]) where
show :: HList '[] -> String
show HList '[]
_ = String
"HNil"
instance (Show a, Show (HList b)) => Show (HList (a ': b)) where
show :: HList (a : b) -> String
show (x
x :+: HList xs
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ x -> String
forall a. Show a => a -> String
show x
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
":+:" String -> ShowS
forall a. [a] -> [a] -> [a]
++ HList xs -> String
forall a. Show a => a -> String
show HList xs
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
instance Semigroup (HList '[]) where
HList '[]
_ <> :: HList '[] -> HList '[] -> HList '[]
<> HList '[]
_ = HList '[]
HNil
instance (Semigroup x, Semigroup (HList xs))
=> Semigroup (HList (x ': xs))
where
(x
x1 :+: HList xs
xs1) <> :: HList (x : xs) -> HList (x : xs) -> HList (x : xs)
<> (x
x2 :+: HList xs
xs2) = (x
x1 x -> x -> x
forall a. Semigroup a => a -> a -> a
<> x
x
x2) x -> HList xs -> HList (x : xs)
forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
:+: (HList xs
xs1 HList xs -> HList xs -> HList xs
forall a. Semigroup a => a -> a -> a
<> HList xs
HList xs
xs2)
instance Monoid (HList '[]) where
mempty :: HList '[]
mempty = HList '[]
HNil
mappend :: HList '[] -> HList '[] -> HList '[]
mappend = HList '[] -> HList '[] -> HList '[]
forall a. Semigroup a => a -> a -> a
(<>)
instance (Semigroup x, Monoid x, Semigroup (HList xs), Monoid (HList xs))
=> Monoid (HList (x ': xs))
where
mempty :: HList (x : xs)
mempty = x
forall a. Monoid a => a
mempty x -> HList xs -> HList (x : xs)
forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
:+: HList xs
forall a. Monoid a => a
mempty
mappend :: HList (x : xs) -> HList (x : xs) -> HList (x : xs)
mappend = HList (x : xs) -> HList (x : xs) -> HList (x : xs)
forall a. Semigroup a => a -> a -> a
(<>)
instance Eq (HList '[]) where
HList '[]
HNil == :: HList '[] -> HList '[] -> Bool
== HList '[]
HNil = Bool
True
HList '[]
HNil /= :: HList '[] -> HList '[] -> Bool
/= HList '[]
HNil = Bool
False
instance (Eq x, Eq (HList xs))
=> Eq (HList (x ': xs))
where
x
x1 :+: HList xs
xr1 == :: HList (x : xs) -> HList (x : xs) -> Bool
== x
x2 :+: HList xs
xr2 = x
x1x -> x -> Bool
forall a. Eq a => a -> a -> Bool
==x
x
x2 Bool -> Bool -> Bool
&& HList xs
xr1HList xs -> HList xs -> Bool
forall a. Eq a => a -> a -> Bool
==HList xs
HList xs
xr2
x
x1 :+: HList xs
xr1 /= :: HList (x : xs) -> HList (x : xs) -> Bool
/= x
x2 :+: HList xs
xr2 = x
x1x -> x -> Bool
forall a. Eq a => a -> a -> Bool
/=x
x
x2 Bool -> Bool -> Bool
|| HList xs
xr1HList xs -> HList xs -> Bool
forall a. Eq a => a -> a -> Bool
/=HList xs
HList xs
xr2
type family Append (l1::[Type]) (l2::[Type]) :: [Type]
type instance Append '[] l2 = l2
type instance Append (car1 ': cdr2) l2 = car1 ': Append cdr2 l2
hAppend :: HList ts1 -> HList ts2 -> HList (Append ts1 ts2)
hAppend :: HList ts1 -> HList ts2 -> HList (Append ts1 ts2)
hAppend HList ts1
HNil HList ts2
l = HList ts2
HList (Append ts1 ts2)
l
hAppend (x
x:+:HList xs
xs) HList ts2
l = x
x x -> HList (Append xs ts2) -> HList (x : Append xs ts2)
forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
:+: HList xs -> HList ts2 -> HList (Append xs ts2)
forall (ts1 :: [*]) (ts2 :: [*]).
HList ts1 -> HList ts2 -> HList (Append ts1 ts2)
hAppend HList xs
xs HList ts2
l
class HInit (l1 :: [Type]) where
hInit :: forall l2 . Proxy l2 -> HList (Append l1 l2) -> HList l1
hSplit :: forall l2 . HList (Append l1 l2) -> (HList l1, HList l2)
instance HInit '[] where
hInit :: Proxy l2 -> HList (Append '[] l2) -> HList '[]
hInit Proxy l2
_ HList (Append '[] l2)
_ = HList '[]
HNil
hSplit :: HList (Append '[] l2) -> (HList '[], HList l2)
hSplit HList (Append '[] l2)
l = (HList '[]
HNil, HList l2
HList (Append '[] l2)
l)
instance HInit l1 => HInit (x ': l1) where
hInit :: Proxy l2 -> HList (Append (x : l1) l2) -> HList (x : l1)
hInit Proxy l2
p (x
x :+: HList xs
xs) = x
x x -> HList l1 -> HList (x : l1)
forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
:+: Proxy l2 -> HList (Append l1 l2) -> HList l1
forall (l1 :: [*]) (l2 :: [*]).
HInit l1 =>
Proxy l2 -> HList (Append l1 l2) -> HList l1
hInit Proxy l2
p HList xs
HList (Append l1 l2)
xs
#if !MIN_VERSION_base(4,9,0)
hInit _ _ = error "cannot happen"
#endif
hSplit :: HList (Append (x : l1) l2) -> (HList (x : l1), HList l2)
hSplit (x
x :+: HList xs
xs) = let (HList l1
l1, HList l2
l2) = HList (Append l1 l2) -> (HList l1, HList l2)
forall (l1 :: [*]) (l2 :: [*]).
HInit l1 =>
HList (Append l1 l2) -> (HList l1, HList l2)
hSplit HList xs
HList (Append l1 l2)
xs
in (x
x x -> HList l1 -> HList (x : l1)
forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
:+: HList l1
l1, HList l2
l2)
#if !MIN_VERSION_base(4,9,0)
hSplit _ = error "cannot happen"
#endif