{-# LANGUAGE CPP #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleContexts #-}

-- | A GADT HList implementation
--
-- There exist other implementations of HList on hackage, but none seem to
-- be reliably maintained.
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)
  -- TCons :: x -> HList xs -> HList (Cons x xs)
  -- TNull :: HList Null

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

-- cannot use the closed variant because of ghc-7.8.4.
-- (was not investigated more closely; there simply
--  is some syntax error for code which works fine with ghc-7.10.)
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" -- see ghc trac #3927
#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