Typed Heterogeneous Lists with DataKinds language extension

HList.hs

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module HList where

import GHC.Exts (Constraint)
import GHC.TypeLits (sing, withSing, Sing, SingI)
import Text.Read (lexP, pfail, readPrec, reset, (+++), Lexeme(..), ReadPrec)
import qualified Text.Read.Lex as L


-- constraint for [*] kind
type family   All (constraint :: * -> Constraint) (as :: [*]) :: Constraint
type instance All constraint '[]       = ()
type instance All constraint (x ': xs) = (constraint x, All constraint xs)


-- Data Definition ----------------

data HList (as :: [*]) where
  HNil :: HList '[]
  HCons :: a -> HList as -> HList (a ': as)


-- Singleton ----------------------

newtype instance Sing (r :: [*]) = SingHList (HList r)

instance SingI '[] where
  sing = SingHList HNil
instance SingI as => SingI (a ': as) where
  sing = let SingHList xs = sing :: Sing as in
         SingHList (HCons undefined xs)


-- Show ----------------------------
  
instance All Show as => Show (HList as) where
  showsPrec = showHListPrec

showHListPrec :: All Show as => Int -> HList as -> ShowS
showHListPrec d xs = showParen (d > 10) $
  showString "HList [" . showHList' xs . showChar ']'
    where
      showHList' :: All Show as => HList as -> ShowS
      showHList' HNil         = id
      showHList' (HCons y ys) = showsPrec (d+1) y
                                . showString (case ys of
                                                HNil      -> ""
                                                HCons _ _ -> ", ")
                                . showHList' ys


-- Read ----------------------------

instance (SingI as, All Read as) => Read (HList as) where
  readPrec = readHList

readHList :: (SingI as, All Read as) => ReadPrec (HList as)
readHList = withSing readHList'
  where
    readHList' :: All Read as => Sing as -> ReadPrec (HList as)
    readHList' (SingHList ts) = do
      Ident "HList" <- lexP
      L.Punc "[" <- lexP
      hlistRest False ts +++ hlistNext ts

    hlistRest :: All Read as => Bool -> HList as -> ReadPrec (HList as)
    hlistRest _ HNil = do
      L.Punc "]" <- lexP
      return HNil
    hlistRest started ts@(HCons _ _) = do
      L.Punc c <- lexP
      case c of
        "," | started -> hlistNext ts
        _             -> pfail

    hlistNext :: All Read as => HList as -> ReadPrec (HList as)
    hlistNext (HCons _ ts) = do
      x  <- reset readPrec
      xs <- hlistRest True ts
      return (HCons x xs)


-- restore HList from [String]
restoreHList :: (SingI as, All Read as) => [String] -> HList as
restoreHList = withSing . restoreHList'
  where
    restoreHList' :: All Read as => [String] -> Sing as -> HList as
    restoreHList' []     (SingHList HNil)         = HNil
    restoreHList' (s:ss) (SingHList (HCons _ ts)) = HCons (read s) (restoreHList' ss (SingHList ts))


-- functions -----------------------

head :: HList (a ': as) -> a
head (HCons x _) = x

tail :: HList (a ': as) -> HList as
tail (HCons _ xs) = xs

infixr 5 .:.
(.:.) :: a -> HList as -> HList (a ': as)
(.:.) = HCons

-- append

type family (m :: [*]) ++ (n :: [*]) :: [*]
type instance '[] ++ ys = ys
type instance (x ': xs) ++ ys = x ': (xs ++ ys)

append :: HList as -> HList bs -> HList (as ++ bs)
append HNil         ys = ys
append (HCons x xs) ys = HCons x (append xs ys)

infixr 5 .++.
(.++.) = append

-- reverse

type Reverse as = Reverse' as '[]
type family   Reverse' (m :: [*]) (n :: [*]) :: [*]
type instance Reverse' '[]       ys = ys
type instance Reverse' (x ': xs) ys = Reverse' xs (x ': ys)

reverse :: HList as -> HList (Reverse as)
reverse xs = reverse' xs HNil
  where
    reverse' :: HList as -> HList bs -> HList (Reverse' as bs)
    reverse' HNil         ys = ys
    reverse' (HCons x xs) ys = reverse' xs (HCons x ys)

HListDef.hs

data HList (as :: [*]) where
  HNil :: HList '[]
  HCons :: a -> HList xs -> HList (a ': xs)

usage-ghci.hs

ghci> :load HList.hs
ghci> :set -XDataKinds 

ghci> let hlist1 = 55 .:. True .:. "hello" .:. HNil :: HList [Int, Bool, String]
ghci> hlist1 
HList [55, True, "hello"]
ghci> read $ show hlist1 :: HList [Int, Bool, String]
HList [55, True, "hello"]

ghci> :t HList.head hlist1
HList.head hlist1 :: Int
ghci> HList.head hlist1
55

ghci> :t HList.tail hlist1
HList.tail hlist1 :: HList [Bool, String]
ghci> HList.tail hlist1
HList [True, "hello"]

ghci> let hlist2 = 'd' .:. [3,5,7] .:. (3.5, "hello") .:. HNil :: HList [Char, [Int], (Double, String)] 
ghci> :t hlist1 .++. hlist2
hlist1 .++. hlist2 :: HList [Int, Bool, String, Char, [Int], (Double, String)]
ghci> hlist1 .++. hlist2
HList [55, True, "hello", 'd', [3,5,7], (3.5,"hello")]

ghci> :t HList.reverse hlist1
HList.reverse hlist1 :: HList [String, Bool, Int]
ghci> HList.reverse hlist1
HList ["hello", True, 55]