58 lines
1.2 KiB
Haskell
58 lines
1.2 KiB
Haskell
{-# LANGUAGE DataKinds #-}
|
|
{-# LANGUAGE GADTs #-}
|
|
{-# LANGUAGE TypeOperators #-}
|
|
{-# LANGUAGE TypeFamilies #-}
|
|
|
|
|
|
-- -- Method 1
|
|
-- data family Hlist (l :: [*])
|
|
-- data instance Hlist '[] = HNil
|
|
-- data instance Hlist (t ': ts) = HCons t (Hlist ts)
|
|
|
|
-- hd :: Hlist (t ': ts) -> t
|
|
-- hd (HCons x _) = x
|
|
|
|
-- tl :: Hlist (t ': ts) -> Hlist ts
|
|
-- tl (HCons _ xs) = xs
|
|
|
|
-- idx :: Hlist ts -> (n :: Int) -> (ts '!! n)
|
|
|
|
-- -- Can't make it work
|
|
-- -- app :: Hlist ts1 -> Hlist ts2 -> Hlist (ts1 '++ ts2)
|
|
-- -- app HNil hls2 = hls2
|
|
|
|
-- -- Can't make it work
|
|
-- -- len :: Hlist ts -> Int
|
|
-- -- len HNil = 0
|
|
-- -- len (HCons _ xs) = 1 + (len xs)
|
|
|
|
|
|
-- -- Method 2 ??
|
|
-- data HNil = HNil
|
|
-- data HCons a b = HCons a b
|
|
|
|
-- a = HCons 3 HNil
|
|
-- b = HCons 3 (HCons True HNil)
|
|
|
|
|
|
|
|
-- -- Method 3
|
|
-- data Hlist :: [*] -> * where
|
|
-- HNil :: Hlist '[]
|
|
-- HCons :: t -> Hlist ts -> Hlist (t : ts)
|
|
|
|
-- data Member x (l':ls) where
|
|
-- First :: Member x (l:ls)
|
|
-- Next :: Member x ls -> Member x (l:ls)
|
|
|
|
-- data Member x (l':ls) where
|
|
-- First :: Member x (l:ls)
|
|
-- Next :: Member x ls -> Member x (l:ls)
|
|
|
|
-- len :: Hlist ts -> Int
|
|
-- len HNil = 0
|
|
-- len (HCons _ xs) = 1 + (len xs)
|
|
|
|
-- a = HCons 3 HNil
|
|
-- b = HCons 3 (HCons True HNil)
|