Extensible field sets, inspired by @aaronlevin’s extensible effects in the Van Laarhoven free monad: http://aaronlevin.ca/post/136494428283/extensible-effects-in-the-van-laarhoven-free-monad

FieldSet.hs

{-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances, GADTs, MultiParamTypeClasses, PolyKinds, TypeOperators #-}
module FieldSet where

infix 9 :=>
-- | We can probably replace this with a wrapper around `Tagged`.
newtype a :=> b = (:=>) b
  deriving (Eq, Show)

-- | “Smart” (actually quite dumb) constructor for the tagged type above for convenience
field :: b -> a :=> b
field = (:=>)

-- | Phantom types for the
data SizeTag
data RangeTag

-- We could also construct this with `':` just like term-level lists: `type Fields = (SizeTag :=> Integer ': RangeTag :=> (Integer, Integer) ': '[])``
type Fields = '[ SizeTag :=> Integer, RangeTag :=> (Integer, Integer) ]
type Info = Record Fields

x :: Info
x = field 0 .:. field (0, 0) .:. RNil

data Record :: [*] -> * where
  RNil :: Record '[]
  RCons :: h -> Record t -> Record (h ': t)

instance (Show h, Show (Record t)) => Show (Record (h ': t)) where
  showsPrec n (RCons h t) = showsPrec n h . showString " : " . showsPrec n t

instance Show (Record '[]) where
  showsPrec _ RNil = ("'[]" ++)

infixr 0 .:.
(.:.) :: h -> Record t -> Record (h ': t)
(.:.) = RCons

class HasField (fields :: [*]) (field :: *) where
  getField :: Record fields -> field

instance {-# OVERLAPPABLE #-} HasField fields field => HasField (notIt ': fields) field where
  getField (RCons _ t) = getField t

instance {-# OVERLAPPABLE #-} HasField (field ': fields) field where
  getField (RCons h _) = h