module Data.OpenRecords
(
Label(..),
KnownSymbol(..),
Rec, Row,
empty,Empty ,
extend, extendUnique, Extend,
rename, renameUnique, Rename,
(.-), (:-),
update,
(.!), (:!),
(.++), (:++),
(.+) , (:+),
(:\), Disjoint, Labels(..), Forall(..), CWit, FWit,
RecOp(..), RowOp(..), (.|), (:|)
)
where
import Data.HashMap.Lazy(HashMap)
import Data.Sequence(Seq,viewl,ViewL(..),(><),(<|))
import qualified Data.HashMap.Lazy as M
import qualified Data.Sequence as S
import Unsafe.Coerce
import Data.List
import GHC.TypeLits
import GHC.Exts
import Data.Type.Equality (type (==))
data Label (s :: Symbol) = Label
instance KnownSymbol s => Show (Label s) where
show = symbolVal
type r :\ l = (LacksP l r ~ LabelUnique l)
type Disjoint l r = (DisjointR l r ~ IsDisjoint)
data HideType where
HideType :: a -> HideType
data Rec (r :: Row *) where
OR :: HashMap String (Seq HideType) -> Rec r
newtype Row a = R [LT a]
empty :: Rec Empty
empty = OR M.empty
type family Empty :: Row * where
Empty = R '[]
extend :: KnownSymbol l => Label l -> a -> Rec r -> Rec (Extend l a r)
extend (show -> l) a (OR m) = OR $ M.insert l v m
where v = HideType a <| M.lookupDefault S.empty l m
extendUnique :: (KnownSymbol l,r :\ l) => Label l -> a -> Rec r -> Rec (Extend l a r)
extendUnique = extend
type family Extend (l :: Symbol) (a :: *) (r :: Row *) :: Row * where
Extend l a (R x) = R (Inject (l :-> a) x)
update :: KnownSymbol l => Label l -> r :! l -> Rec r -> Rec r
update (show -> l) a (OR m) = OR $ M.adjust f l m where f = S.update 0 (HideType a)
rename :: (KnownSymbol l, KnownSymbol l') => Label l -> Label l' -> Rec r -> Rec (Rename l l' r)
rename l l' r = extend l' (r .! l) (r .- l)
renameUnique :: (KnownSymbol l, KnownSymbol l', r :\ l') => Label l -> Label l' -> Rec r -> Rec (Rename l l' r)
renameUnique = rename
type family Rename (l :: Symbol) (l' :: Symbol) (r :: Row *) :: Row * where
Rename l l' r = Extend l' (r :! l) (r :- l)
infix 8 .-
(.!) :: KnownSymbol l => Rec r -> Label l -> r :! l
(OR m) .! (show -> a) = x'
where x S.:< t = S.viewl $ m M.! a
x' = case x of HideType p -> unsafeCoerce p
infixl 6 :!
type family (r :: Row *) :! (t :: Symbol) :: * where
(R r) :! l = Get l r
(.-) :: KnownSymbol l => Rec r -> Label l -> Rec (r :- l)
(OR m) .- (show -> a) = OR m'
where x S.:< t = S.viewl $ m M.! a
m' = case S.viewl t of
EmptyL -> M.delete a m
_ -> M.insert a t m
type family (r :: Row *) :- (s :: Symbol) :: Row * where
(R r) :- l = R (Remove l r)
(.++) :: Rec l -> Rec r -> Rec (l :++ r)
(OR l) .++ (OR r) = OR $ M.unionWith (><) l r
type family (l :: Row *) :++ (r :: Row *) :: Row * where
(R l) :++ (R r) = R (Merge l r)
(.+) :: Disjoint l r => Rec l -> Rec r -> Rec (l :+ r)
(OR l) .+ (OR r) = OR $ M.unionWith (error "Impossible") l r
type family (l :: Row *) :+ (r :: Row *) :: Row * where
(R l) :+ (R r) = R (Merge l r)
class NoConstr a
instance NoConstr a
class (r :\ l) => Lacks (l :: Symbol) (r :: Row *)
instance (r :\ l) => Lacks l r
class ((r :! l) ~ a ) => HasType l a r
instance ((r :! l) ~ a ) => HasType l a r
infix 5 :=
infix 5 :!=
infix 5 :<-
data RecOp (c :: Row * -> Constraint) (rowOp :: RowOp *) where
(:<-) :: KnownSymbol l => Label l -> a -> RecOp (HasType l a) RUp
(:=) :: KnownSymbol l => Label l -> a -> RecOp NoConstr (l ::= a)
(:!=) :: KnownSymbol l => Label l -> a -> RecOp (Lacks l) (l ::= a)
(:<-|) :: (KnownSymbol l, KnownSymbol l') => Label l' -> Label l -> RecOp NoConstr (l' ::<-| l)
(:<-!) :: (KnownSymbol l, KnownSymbol l', r :\ l') => Label l' -> Label l -> RecOp (Lacks l') (l' ::<-| l)
infix 5 ::=
infix 5 ::<-|
data RowOp (a :: *) where
RUp :: RowOp a
(::=) :: Symbol -> a -> RowOp a
(::<-|) :: Symbol -> Symbol -> RowOp a
infixr 4 .|
(.|) :: c r => RecOp c ro -> Rec r -> Rec (ro :| r)
(l :<- a) .| m = update l a m
(l := a) .| m = extend l a m
(l :!= a) .| m = extendUnique l a m
(l' :<-| l) .| m = rename l l' m
(l' :<-! l) .| m = renameUnique l l' m
infixr 4 :|
type family (x :: RowOp *) :| (r :: Row *) :: Row * where
RUp :| r = r
(l ::= a) :| r = Extend l a r
(l' ::<-| l) :| r = Rename l l' r
class Labels (r :: Row *) where
labels :: Rec r -> [String]
instance Labels (R '[]) where
labels _ = []
instance (KnownSymbol l , Labels (R t)) => Labels (R (l :-> v ': t)) where
labels r = show l : labels (r .- l) where l = Label :: Label l
data CWit (c :: * -> Constraint) = CWit
class Forall (r :: Row *) (c :: * -> Constraint) where
rinit :: CWit c -> (forall a. c a => a) -> Rec r
erase :: CWit c -> (forall a. c a => a -> b) -> Rec r -> [b]
eraseZip :: CWit c -> (forall a. c a => a -> a -> b) -> Rec r -> Rec r -> [b]
data FWit (f :: * -> *) = FWit
class RowMap (f :: * -> *) (r :: Row *) where
type Map f r :: Row *
rmap :: FWit f -> (forall a. a -> f a) -> Rec r -> Rec (Map f r)
instance RowMapx f r => RowMap f (R r) where
type Map f (R r) = R (RM f r)
rmap = rmap'
class RowMapx (f :: * -> *) (r :: [LT *]) where
type RM f r :: [LT *]
rmap' :: FWit f -> (forall a. a -> f a) -> Rec (R r) -> Rec (R (RM f r))
instance RowMapx f '[] where
type RM f '[] = '[]
rmap' _ _ _ = empty
instance (KnownSymbol l, RowMapx f t) => RowMapx f (l :-> v ': t) where
type RM f (l :-> v ': t) = l :-> f v ': RM f t
rmap' w f r = unsafeInjectFront l (f (r .! l)) (rmap' w f (r .- l))
where l = Label :: Label l
class RowMapC (c :: * -> Constraint) (f :: * -> *) (r :: Row *) where
type MapC c f r :: Row *
rmapc :: CWit c -> FWit f -> (forall a. c a => a -> f a) -> Rec r -> Rec (MapC c f r)
instance RMapc c f r => RowMapC c f (R r) where
type MapC c f (R r) = R (RMapp c f r)
rmapc = rmapc'
class RMapc (c :: * -> Constraint) (f :: * -> *) (r :: [LT *]) where
type RMapp c f r :: [LT *]
rmapc' :: CWit c -> FWit f -> (forall a. c a => a -> f a) -> Rec (R r) -> Rec (R (RMapp c f r))
instance RMapc c f '[] where
type RMapp c f '[] = '[]
rmapc' _ _ _ _ = empty
instance (KnownSymbol l, c v, RMapc c f t) => RMapc c f (l :-> v ': t) where
type RMapp c f (l :-> v ': t) = l :-> f v ': RMapp c f t
rmapc' c w f r = unsafeInjectFront l (f (r .! l)) (rmapc' c w f (r .- l))
where l = Label :: Label l
instance Forall (R '[]) c where
rinit _ _ = empty
erase _ _ _ = []
eraseZip _ _ _ _ = []
instance (KnownSymbol l, Forall (R t) c, c a) => Forall (R (l :-> a ': t)) c where
rinit c f = unsafeInjectFront l f (rinit c f) where l = Label :: Label l
erase c f r = f (r .! l) : erase c f (r .- l) where l = Label :: Label l
eraseZip c f x y = (f (x .! l) (y .! l)) : eraseZip c f (x .- l) (y .- l) where
l = Label :: Label l
class RowZip (r1 :: Row *) (r2 :: Row *) where
type RZip r1 r2 :: Row *
rzip :: Rec r1 -> Rec r2 -> Rec (RZip r1 r2)
instance RZipt r1 r2 => RowZip (R r1) (R r2) where
type RZip (R r1) (R r2) = R (RZipp r1 r2)
rzip = rzip'
class RZipt (r1 :: [LT *]) (r2 :: [LT *]) where
type RZipp r1 r2 :: [LT *]
rzip' :: Rec (R r1) -> Rec (R r2) -> Rec (R (RZipp r1 r2))
instance RZipt '[] '[] where
type RZipp '[] '[] = '[]
rzip' _ _ = empty
instance (KnownSymbol l, RZipt t1 t2) =>
RZipt (l :-> v1 ': t1) (l :-> v2 ': t2) where
type RZipp (l :-> v1 ': t1) (l :-> v2 ': t2) = l :-> (v1,v2) ': RZipp t1 t2
rzip' r1 r2 = unsafeInjectFront l (r1 .! l, r2 .! l) (rzip' (r1 .- l) (r2 .- l))
where l = Label :: Label l
instance (Labels r, Forall r Show) => Show (Rec r) where
show r = "{ " ++ meat ++ " }"
where meat = intercalate ", " binds
binds = zipWith (\x y -> x ++ "=" ++ y) ls vs
ls = labels r
vs = erase (CWit :: CWit Show) show r
instance (Forall r Eq) => Eq (Rec r) where
r == r' = and $ eraseZip (CWit :: CWit Eq) (==) r r'
instance (Eq (Rec r), Forall r Ord) => Ord (Rec r) where
compare m m' = cmp $ eraseZip (CWit :: CWit Ord) compare m m'
where cmp l | [] <- l' = EQ
| a : _ <- l' = a
where l' = dropWhile (== EQ) l
instance (Forall r Bounded) => Bounded (Rec r) where
minBound = rinit (CWit :: CWit Bounded) minBound
maxBound = rinit (CWit :: CWit Bounded) maxBound
unsafeInjectFront :: KnownSymbol l => Label l -> a -> Rec (R r) -> Rec (R (l :-> a ': r))
unsafeInjectFront (show -> a) b (OR m) = OR $ M.insert a v m
where v = HideType b <| M.lookupDefault S.empty a m
data LT a = Symbol :-> a
data Unique = LabelUnique Symbol | LabelNotUnique Symbol
type family Inject (l :: LT *) (r :: [LT *]) where
Inject (l :-> t) '[] = (l :-> t ': '[])
Inject (l :-> t) (l' :-> t' ': x) =
Ifte (l <=.? l')
(l :-> t ': l' :-> t' ': x)
(l' :-> t' ': Inject (l :-> t) x)
type family Ifte (c :: Bool) (t :: [LT *]) (f :: [LT *]) where
Ifte True t f = t
Ifte False t f = f
data NoSuchField (s :: Symbol)
type family Get (l :: Symbol) (r :: [LT *]) where
Get l '[] = NoSuchField l
Get l (l :-> t ': x) = t
Get l (l' :-> t ': x) = Get l x
type family Remove (l :: Symbol) (r :: [LT *]) where
Remove l (l :-> t ': x) = x
Remove l (l' :-> t ': x) = l' :-> t ': Remove l x
type family LacksP (l :: Symbol) (r :: Row *) where
LacksP l (R r) = LacksR l r
type family LacksR (l :: Symbol) (r :: [LT *]) where
LacksR l '[] = LabelUnique l
LacksR l (l :-> t ': x) = LabelNotUnique l
LacksR l (p ': x) = LacksR l x
type family Merge (l :: [LT *]) (r :: [LT *]) where
Merge '[] r = r
Merge l '[] = l
Merge (hl :-> al ': tl) (hr :-> ar ': tr) =
Ifte (hl <=.? hr)
(hl :-> al ': Merge tl (hr :-> ar ': tr))
(hr :-> ar ': Merge (hl :-> al ': tl) tr)
data DisjointErr = IsDisjoint | Duplicate Symbol
type family IfteD (c :: Bool) (t :: DisjointErr) (f :: DisjointErr) where
IfteD True t f = t
IfteD False t f = f
type family DisjointR (l :: Row *) (r :: Row *) where
DisjointR (R l) (R r) = DisjointZ l r
type family DisjointZ (l :: [LT *]) (r :: [LT *]) where
DisjointZ '[] r = IsDisjoint
DisjointZ l '[] = IsDisjoint
DisjointZ (l :-> al ': tl) (l :-> ar ': tr) = Duplicate l
DisjointZ (hl :-> al ': tl) (hr :-> ar ': tr) =
IfteD (hl <=.? hr)
(DisjointZ tl (hr :-> ar ': tr))
(DisjointZ (hl :-> al ': tl) tr)
type a <=.? b = (CmpSymbol a b == 'LT)