Extensible records with data kinds

ExtensibleRecords.hs

{-# 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")