Folding type level lists using type level monoids

typemonoids.hs

{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, TypeOperators, EmptyDataDecls, GADTs #-}

import Data.Proxy
import Data.Void
import Unsafe.Coerce

type family Foldr (append :: a -> b -> b) (zero :: b) fa :: b where
  Foldr append zero '[] = zero;
  Foldr append zero (x ': xs) = append x (Foldr append zero xs)

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

infixr 6 :::

choose :: Int -> d -> HList l -> Foldr Either d l
choose n d HNil       = d
choose 0 _ (t ::: _)  = Left t
choose n d (_ ::: ts) = Right $ choose (n - 1) d ts

-- choose 1 () (1 ::: "foo" ::: HNil) == Right (Left "")
-- choose 1 () HNil                   == ()
-- choose 1 () ("bar ::: HNil)        == Right 1