mirror of
https://github.com/ilyakooo0/tuple-morph.git
synced 2024-08-16 01:40:32 +03:00
45 lines
1.2 KiB
Haskell
45 lines
1.2 KiB
Haskell
{-# LANGUAGE PolyKinds #-}
|
|
{-# LANGUAGE DataKinds #-}
|
|
{-# LANGUAGE TypeOperators #-}
|
|
{-# LANGUAGE TypeFamilies #-}
|
|
{- |
|
|
Module : Data.Tuple.Morph.Append
|
|
Description : Appending type lists.
|
|
Copyright : (c) Paweł Nowak
|
|
License : MIT
|
|
|
|
Maintainer : Paweł Nowak <pawel834@gmail.com>
|
|
Stability : experimental
|
|
|
|
Appending type lists and HLists.
|
|
-}
|
|
module Data.Tuple.Morph.Append where
|
|
|
|
import Data.HList.HList (HList(..))
|
|
import Data.Proxy
|
|
import Data.Type.Equality
|
|
import Unsafe.Coerce
|
|
|
|
infixr 5 ++, ++@
|
|
|
|
-- | Appends two type lists.
|
|
type family (++) (a :: [k]) (b :: [k]) :: [k] where
|
|
'[] ++ b = b
|
|
(a ': as) ++ b = a ': (as ++ b)
|
|
|
|
-- TODO: Proofs could use some love when GHC 7.10 comes out.
|
|
|
|
-- | Proof (by unsafeCoerce) that appending is associative.
|
|
appendAssoc :: Proxy a -> Proxy b -> Proxy c
|
|
-> ((a ++ b) ++ c) :~: (a ++ (b ++ c))
|
|
appendAssoc _ _ _ = unsafeCoerce Refl
|
|
|
|
-- | Proof (by unsafeCoerce) that '[] is a right identity of (++).
|
|
appendRightId :: Proxy a -> (a ++ '[]) :~: a
|
|
appendRightId _ = unsafeCoerce Refl
|
|
|
|
-- | Appends two HLists.
|
|
(++@) :: HList a -> HList b -> HList (a ++ b)
|
|
HNil ++@ ys = ys
|
|
(HCons x xs) ++@ ys = HCons x (xs ++@ ys)
|