HAList.hs

{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, TypeOperators, GADTs
           , OverlappingInstances, FlexibleInstances, UndecidableInstances
           , MultiParamTypeClasses
           #-}

import GHC.TypeLits
import Data.Type.Equality
import Data.Proxy

--------------------------------------------------------------------------------
--  Heterogeneous Association Lists
--------------------------------------------------------------------------------

data HAList :: [(Symbol,*)] -> * where
    ANil  :: HAList '[]
    ACons :: a -> HAList ts -> HAList ('(key,a) ': ts)

--------------------------------------------------------------------------------
--  type-level Find
--------------------------------------------------------------------------------

type family If (p :: Bool) (a :: k) (b :: k) :: k where
    If 'True a b = a
    If 'False a b = b

type family Find (k :: a) (ls :: [(a,b)]) :: b
type instance Find k ('(a,b) ': xs) = If (a == k) b (Find k xs)

-- -- Another way to implement Find, with closed type families
-- -- fusing If and Find with keys unified on site
-- -- to avoid nested type family application and thus -XUndecidableInstances
-- data Btm
-- type family Find (k :: a) (ls :: [(a,b)]) :: b where
--     Find k ('(k     ,b) ': xs) = b
--     Find k ('(not_k ,b) ': xs) = Find k xs
--     Find k '[]                = Btm


--------------------------------------------------------------------------------
--  term-level Find
--------------------------------------------------------------------------------

-- associate terms and types with ad-hoc polymorphisms
-- sadly we don't have closed-form type classes, but -XOverlappingInstances would do
class Findable k xs where
    find :: Proxy k -> HAList xs -> Find k xs

instance Findable k ('(k, x) ': xs) where
    find _ (ACons x _) = x

-- pre-conditions:
--  1. Find k ('(not_k, x) ': xs) ~ Find k xs
--  2. Findable k xs
instance (Find k ('(not_k, x) ': xs) ~ Find k xs
        , Findable k xs)
       => Findable k ('(not_k, x) ': xs) where
    find k (ACons x xs) = find k xs

-- -- unreachable case, uninhabited because of Find
-- instance Findable k '[] where
--     find _ _ = undefined

--------------------------------------------------------------------------------
--  examples
--------------------------------------------------------------------------------

haEmpty :: HAList '[]
haEmpty = ANil

haA :: HAList '[ '("A", Bool) ]
haA = ACons True ANil

haAB :: HAList '[ '("A", Bool), '("B", Char) ]
haAB = ACons True (ACons 'a' ANil)

keyA :: Proxy "A"
keyA = Proxy

keyB :: Proxy "B"
keyB = Proxy