@@ -5,13 +5,14 @@ The implementation is similar to that shown in the paper.
55{-# LANGUAGE TypeOperators, PolyKinds, DataKinds, KindSignatures,
66 TypeFamilies, UndecidableInstances, MultiParamTypeClasses,
77 FlexibleInstances, GADTs, FlexibleContexts, ScopedTypeVariables,
8− ConstraintKinds #-}
8+ ConstraintKinds, IncoherentInstances #-}
99
1010module Data.Type.Map (Mapping(..), Union, Unionable, union, Var(..), Map(..),
1111 Combine, Combinable(..), Cmp,
1212 Nubable, nub,
1313 Lookup, Member, (:\), Split, split,
14− IsMap, AsMap, asMap,
14+ IsMember, lookp, Updatable, update,
15+ IsMap, AsMap, asMap,
1516 Submap, submap) where
1617
1718import GHC.TypeLits
@@ -75,6 +76,33 @@ data Map (n :: [Mapping Symbol *]) where
7576 Empty :: Map '[]
7677 Ext :: Var k -> v -> Map m -> Map ((k :-> v) ': m)
7778
79+{-| Membership test a type class (predicate) -}
80+class IsMember v t m where
81+ {-| Value-level lookup of elements from a map, via type class predicate -}
82+ lookp :: Var v -> Map m -> t
83+
84+instance {-# OVERLAPS #-} IsMember v t ((v ':-> t) ': m) where
85+ lookp _ (Ext _ x _) = x
86+
87+instance IsMember v t m => IsMember v t (x ': m) where
88+ lookp v (Ext _ _ m) = lookp v m
89+
90+
91+{-| Updatability as a type class -}
92+class Updatable v t m n where
93+ {-| Update a map with `m` at variable `v` with a value of type `t`
94+ to produce a map of type `n` -}
95+ update :: Map m -> Var v -> t -> Map n
96+
97+instance {-# OVERLAPS #-} Updatable v t ((v ':-> s) ': m) ((v ':-> t) ': m) where
98+ update (Ext v _ m) _ x = Ext v x m
99+
100+instance Updatable v t m n => Updatable v t ((w ':-> y) ': m) ((w ':-> y) ': n) where
101+ update (Ext w y m) v x = Ext w y (update m v x)
102+
103+instance Updatable v t '[] '[v ':-> t] where
104+ update Empty v x = Ext v x Empty
105+
78106{-| Predicate to check if in normalised map form -}
79107type IsMap s = (s ~ Nub (Sort s))
80108