59 lines
1.2 KiB
Haskell
59 lines
1.2 KiB
Haskell
{-# LANGUAGE DataKinds #-}
|
|
{-# LANGUAGE GADTs #-} -- Enabled by default apparently
|
|
{-# LANGUAGE TypeOperators #-} -- Enabled by default apparently
|
|
{-# LANGUAGE TypeFamilies #-}
|
|
|
|
data Hlist :: [*] -> * where
|
|
HNil :: Hlist '[]
|
|
HCons :: t -> Hlist ts -> Hlist (t : ts)
|
|
|
|
data Member :: a -> [*] -> * where
|
|
First :: Member x (x':l)
|
|
Next :: Member x l -> Member x (x':l)
|
|
|
|
-- data Member x (l':ls) where
|
|
-- First :: Member x (l:ls)
|
|
-- Next :: Member x ls -> Member x (l:ls)
|
|
|
|
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]
|