69 lines
1.4 KiB
Haskell
69 lines
1.4 KiB
Haskell
{-# LANGUAGE DataKinds #-}
|
|
{-# LANGUAGE GADTs #-} -- Enabled by default apparently
|
|
{-# LANGUAGE TypeOperators #-} -- Enabled by default apparently
|
|
{-# LANGUAGE TypeFamilies #-}
|
|
|
|
|
|
data HList :: (* -> *) -> [*] -> * where
|
|
HNil :: HList f '[]
|
|
HCons :: f t -> HList f ts -> HList f (t':ts)
|
|
|
|
|
|
-- Example hlists
|
|
-- a = HCons 3 HNil
|
|
|
|
|
|
|
|
|
|
---------------------------------------------------------------------------
|
|
|
|
-- data Hlist :: [*] -> * where
|
|
-- HNil :: Hlist '[]
|
|
-- HCons :: t -> Hlist ts -> Hlist (t : ts)
|
|
|
|
-- data Member :: a -> [*] -> * where
|
|
-- First :: Member x (y:l)
|
|
-- Next :: Member x l -> Member x (y:l)
|
|
|
|
-- hd :: Hlist (t ': ts) -> t
|
|
-- hd (HCons x _) = x
|
|
|
|
-- tl :: Hlist (t ': ts) -> Hlist ts
|
|
-- tl (HCons _ xs) = xs
|
|
|
|
-- len :: Hlist ts -> Int
|
|
-- len HNil = 0
|
|
-- len (HCons _ xs) = 1 + (len xs)
|
|
|
|
-- type family (++) (l1 :: [*]) (l2 :: [*]) where
|
|
-- '[] ++ y = y
|
|
-- (x':xs) ++ y = x':(xs ++ y)
|
|
|
|
-- cat :: Hlist ts1 -> Hlist ts2 -> Hlist (ts1 ++ ts2)
|
|
-- cat HNil y = y
|
|
-- cat (HCons x xs) y = HCons x (cat xs y)
|
|
|
|
|
|
|
|
|
|
-- -- Example hlists
|
|
-- a = HCons 3 HNil
|
|
-- b = HCons 3 (HCons True HNil)
|
|
-- -- λ> a
|
|
-- -- a :: Hlist '[Integer]
|
|
-- -- λ> b
|
|
-- -- b :: Hlist '[Integer, Bool]
|
|
-- -- λ> tl a
|
|
-- --
|
|
-- -- tl a :: Hlist '[]
|
|
-- -- λ> tl b
|
|
-- -- tl b :: Hlist '[Bool]
|
|
-- -- λ> hd a
|
|
-- -- 3
|
|
-- -- λ> hd (tl b)
|
|
-- -- True
|
|
-- -- λ> hd $ tl (tl b) -- Error
|
|
-- --
|
|
-- -- λ> cat b b
|
|
-- -- cat b b :: Hlist '[Integer, Bool, Integer, Bool]
|