{-# LANGUAGE TypeOperators, ScopedTypeVariables, MultiParamTypeClasses, TypeFamilies, FlexibleInstances, UndecidableInstances #-} {- module Records: type-safe polymorphic extensible records with union & update Copyright 2007, Barnaby P. Hilken. Permission to use this for non-commercial purposes is given, provided I am acknowledged in all derived works. ********************************************************************************************* * * * To use records, you must declare a set of labels, which are both conid and tycon. * * For each label N, define: * * * * data N = N deriving (Eq, Ord, Show) * * * * For each pair of labels N, M define ONE of: * * * * type instance NameCmp N M = NameLT * * type instance NameCmp N N = NameEQ * * type instance NameCmp N M = NameGT * * * * in such a way as to order the labels linearly. Someday, Haskell may do this for you! * * * ********************************************************************************************* Record construction: EmptyRec is the empty record. N =: x is the record with one field labelled N carrying data x. t +: u is the union of records t and u. Any overlap of labels gives a static error. Record destruction: t .: N is the value of field N in record t. A lack of field N gives a static error. t -: N is record t with field N deleted. A lack of field N gives a static error. Record update: t |: u is the record with fields from u where it has them, t otherwise. If u has any fields not in t, or of different types from t, there is a static error. Note that the result has the same type as t. All these records have types: EmptyRec is the type of the empty record. N :=: a is the type of a record with one field labelled N carrying data of type a. r :+: s is the union of record types r and s. Any overlap of labels gives a static error. r :.: N is the type of field N in a record of type r. A lack of field N gives a static error. r :-: N is record type r with field N deleted. A lack of field N gives a static error. Finally some classes to govern the polymorphism: r `Contains` N means that r is a record type with a field labelled N. r `Disjoint` s means that r and s are record types with no fields in common. r `Subrecord` s means that r and s are record types, and every field of r also occurs in s (with the same type). The types of the basic operators are as follows: (=:) :: n -> a -> n :=: a (+:) :: r `Disjoint` s => r -> s -> r :+: s (.:) :: r `Contains` n => r -> n -> r :.: n (-:) :: r `Contains` n => r -> n -> r :-: n (|:) :: r `Subrecord` s => s -> r -> s -} module Records (EmptyRec(..), (:=:), (=:), (:.:), (.:), (:-:), (-:), (:+:), (+:), (|:), Contains, Disjoint, Subrecord, NameLT(..), NameEQ(..), NameGT(..), NameCmp) where infixr 4 :=:, =: infixl 3 :.:, .:, :-:, -:, :+:, +:, |: infix 2 `Contains`, `Disjoint`, `Subrecord` type family NameCmp n m data NameLT = NameLT data NameEQ = NameEQ data NameGT = NameGT data EmptyRec = EmptyRec deriving (Eq, Ord) data Record n a r = Record n a r deriving (Eq, Ord) instance Show EmptyRec where showsPrec (-1) EmptyRec = id showsPrec j EmptyRec = showString "{}" instance (Show n, Show a, Show r) => Show (Record n a r) where showsPrec (-1) (Record n x r) = showString ", " . shows n . showString "=" . shows x . showsPrec (-1) r showsPrec j (Record n x r) = showChar '{' . shows n . showString "=" . shows x . showsPrec (-1) r . showChar '}' type n :=: a = Record n a EmptyRec (=:) :: n -> a -> n :=: a n =: x = Record n x EmptyRec class r `Contains` n where type (:.:) r n :: * type (:-:) r n :: * (.:) :: r -> n -> r :.: n (-:) :: r -> n -> r :-: n class RecCont cmp r n where type RecProj cmp r n :: * type RecDel cmp r n :: * recProj :: cmp -> r -> n -> RecProj cmp r n recDel :: cmp -> r -> n -> RecDel cmp r n instance RecCont (NameCmp n m) (Record n a r) m => Contains (Record n a r) m where type Record n a r :.: m = RecProj (NameCmp n m) (Record n a r) m type Record n a r :-: m = RecDel (NameCmp n m) (Record n a r) m t .: m = recProj (undefined::NameCmp n m) t m t -: m = recDel (undefined::NameCmp n m) t m instance RecCont NameEQ (Record n a r) m where type RecProj NameEQ (Record n a r) m = a type RecDel NameEQ (Record n a r) m = r recProj _ (Record n x t) m = x recDel _ (Record n x t) m = t instance Contains r m => RecCont NameLT (Record n a r) m where type RecProj NameLT (Record n a r) m = r :.: m type RecDel NameLT (Record n a r) m = Record n a (r :-: m) recProj _ (Record n x t) m = t .: m recDel _ (Record n x t) m = Record n x (t -: m) class r `Disjoint` s where type (:+:) r s :: * (+:) :: r -> s -> r :+: s class RecDisj cmp r s where type RecUnion cmp r s :: * recUnion :: cmp -> r -> s -> RecUnion cmp r s instance Disjoint EmptyRec r where type EmptyRec :+: r = r EmptyRec +: t = t instance Disjoint (Record n a r) EmptyRec where type Record n a r :+: EmptyRec = Record n a r t +: EmptyRec = t instance RecDisj (NameCmp n m) (Record n a r) (Record m b s) => Disjoint (Record n a r) (Record m b s) where type Record n a r :+: Record m b s = RecUnion (NameCmp n m) (Record n a r) (Record m b s) t +: u = recUnion (undefined::NameCmp n m) t u instance Disjoint r (Record m b s) => RecDisj NameLT (Record n a r) (Record m b s) where type RecUnion NameLT (Record n a r) (Record m b s) = Record n a (r :+: Record m b s) recUnion _ (Record n x t) u = Record n x (t +: u) instance Disjoint (Record n a r) s => RecDisj NameGT (Record n a r) (Record m b s) where type RecUnion NameGT (Record n a r) (Record m b s) = Record m b (Record n a r :+: s) recUnion _ t (Record n x u) = Record n x (t +: u) class r `Subrecord` s where (|:) :: s -> r -> s class RecSub cmp r s where recUpdate :: cmp -> s -> r -> s instance Subrecord EmptyRec r where t |: EmptyRec = t instance RecSub (NameCmp n m) (Record n a r) (Record m b s) => Subrecord (Record n a r) (Record m b s) where t |: u = recUpdate (undefined::NameCmp n m) t u instance Subrecord r s => RecSub NameEQ (Record n a r) (Record n a s) where recUpdate _ (Record m y t) (Record n x u) = Record n x (t |: u) instance Subrecord (Record n a r) s => RecSub NameGT (Record n a r) (Record m b s) where recUpdate _ (Record m y t) u = Record m y (t |: u)