Skip to content

Instantly share code, notes, and snippets.

@hesselink
Created April 25, 2012 20:05
Show Gist options
  • Save hesselink/2492939 to your computer and use it in GitHub Desktop.
Save hesselink/2492939 to your computer and use it in GitHub Desktop.
Extensible records with data kinds
{-# LANGUAGE
GADTs
, KindSignatures
, DataKinds
, PolyKinds
, TypeOperators
, TypeFamilies
, MultiParamTypeClasses
, FlexibleInstances
, UndecidableInstances
, ScopedTypeVariables
, FlexibleContexts
, ConstraintKinds
, StandaloneDeriving
#-}
module Main where
import GHC.Prim
import GHC.TypeLits
-- * Equality on types. Hopefully will be provided at least for
-- Symbols.
type family TEq (x :: k) (y :: k) :: Bool
type instance TEq "aap" "aap" = True
type instance TEq "aap" "noot" = False
type instance TEq "aap" "mies" = False
type instance TEq "noot" "aap" = False
type instance TEq "noot" "noot" = True
type instance TEq "noot" "mies" = False
type instance TEq "mies" "aap" = False
type instance TEq "mies" "noot" = False
type instance TEq "mies" "mies" = True
-- * The type of field 'f' in the list of field/type pairs 'fs'.
-- Basically 'lookup' on types.
type family FieldType (f :: Symbol) fs :: *
type instance FieldType f ('(f', a)':fs) = FieldType' (TEq f f') f ('(f', a)':fs)
type family FieldType' (b :: Bool) (f :: Symbol) fs :: *
type instance FieldType' True f ('(f , a)':fs) = a
type instance FieldType' False f ('(f', a)':fs) = FieldType f fs
-- * Require a constraint on all types in a record. Useful for e.g.
-- Show.
type family All (c :: a -> Constraint) (fs :: [(Symbol, *)]) :: Constraint
type instance All c '[] = ()
type instance All c ('(f,a) ': fs) = (c a, All c fs)
-- * A Record is a list of values, where the types are paired with the
-- field name.
data Record :: [(Symbol, *)] -> * where
Empty :: Record '[]
Field :: a -> Record fs -> Record ('(f,a)':fs)
deriving instance All Show fs => Show (Record fs)
data Proxy a = Proxy
-- * The class 'Has' means that the list 'fs' contains a tuple with
-- first component 'f'. The 'get' function returns the value of that
-- field in a 'Record', which is given by the 'FieldType' type family.
-- The implementation immediately recurses with the result of the type
-- equality between the field 'f', and the field at the head of the
-- record contents, following the implementation of FieldType.
-- 'modify' works similarly.
class Has (f :: Symbol) fs where
get :: Proxy f -> Record fs -> FieldType f fs
modify :: Proxy f -> (FieldType f fs -> FieldType f fs) -> Record fs -> Record fs
instance Has' (TEq f f') f ('(f',a)':fs) => Has (f :: Symbol) (('(f',a)':fs) :: [(Symbol, *)]) where
get = get' (Proxy :: Proxy (TEq f f'))
modify = modify' (Proxy :: Proxy (TEq f f'))
class Has' (b :: Bool) (f :: Symbol) fs where
get' :: Proxy b -> Proxy f -> Record fs -> FieldType' b f fs
modify' :: Proxy b -> Proxy f -> (FieldType' b f fs -> FieldType' b f fs) -> Record fs -> Record fs
instance Has' True f ('(f,a)':fs) where
get' bp fp (Field v r) = v
modify' bp fp f (Field v r) = Field (f v) r
instance Has f fs => Has' False f ('(f',a)':fs) where
get' bp fp (Field v r) = get fp r
modify' bp fp f (Field v r) = Field v (modify fp f r)
-- * Examples
r1 :: Record '[ '("aap", Integer) ]
r1 = Field 1 Empty
getAapFromR1 :: Integer
getAapFromR1 = get (Proxy :: Proxy "aap") r1
r2 :: Record '[ '("noot", String), '("aap", Integer) ]
r2 = Field "hello" (Field 3 Empty)
getAapFromR2 :: Integer
getAapFromR2 = get (Proxy :: Proxy "aap") r2
getAap :: Has "aap" fs => Record fs -> FieldType "aap" fs
getAap = get (Proxy :: Proxy "aap")
modifyAap :: Has "aap" fs => (FieldType "aap" fs -> FieldType "aap" fs) -> Record fs -> Record fs
modifyAap = modify (Proxy :: Proxy "aap")
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment