PureScript HList

hlist.purs

module Data.HList where

import Data.Semiring ((+))
import Prim.RowList (Cons, Nil, kind RowList)
import Type.Data.RowList (RLProxy)
import Type.Equality (class TypeEquals)

newtype HList (xs :: RowList) = HList forall r
  .   (forall y ys. TypeEquals (RLProxy xs) (RLProxy (Cons "" y ys)) => y -> HList ys -> r)
  ->  (TypeEquals (RLProxy xs) (RLProxy Nil) => r)
  ->  r
--

cons :: forall x xs. x -> HList xs -> HList (Cons "" x xs)
cons x xs = HList (\c n -> c x xs)

infixr 6 cons as :

nil :: HList Nil
nil = HList (\_ n -> n)

length :: forall xs. HList xs -> Int
length = go 0
  where
  go :: forall ys. Int -> HList ys -> Int
  go n (HList f) = f (\_ r -> go (n + 1) r) n
--