to/from HList

hlist.hs

{-# LANGUAGE TypeFamilies, DataKinds, ScopedTypeVariables, RankNTypes, GADTs, TypeOperators #-}

module HListFL where

data Nat = Z | S Nat

data Natty n where
  Zy :: Natty 'Z
  Sy :: Natty n -> Natty ('S n)

type family Replicate n a where
  Replicate 'Z a = '[]
  Replicate ('S n) a = a ': Replicate n a

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

data FromListResult a where
  FromListResult :: Natty n -> HList (Replicate n a) -> FromListResult a

fromList :: [a] -> FromListResult a
fromList [] = FromListResult Zy HNil
fromList (a : as) = case fromList as of
  FromListResult n xs -> FromListResult (Sy n) (HCons a xs)

toList :: FromListResult a -> [a]
toList (FromListResult n xs) = toList' n xs

toList' :: Natty n -> HList (Replicate n a) -> [a]
toList' Zy (xs :: HList '[]) = case xs of HNil -> []
toList' (Sy (n :: Natty n)) (HCons x xs :: HList (a ': Replicate n a)) = x : toList' n xs