Skip to content

Instantly share code, notes, and snippets.

@banacorn
Created Jan 15, 2016
Embed
What would you like to do?
{-# 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment