public
Created

Extensible records with data kinds

  • Download Gist
ExtensibleRecords.hs
Haskell
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106
{-# 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")

Please sign in to comment on this gist.

Something went wrong with that request. Please try again.