-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Type-level sets and finite maps (with value-level counterparts)
--   
--   This package provides type-level sets (no duplicates, sorted to
--   provide a normal form) via <a>Set</a> and type-level finite maps via
--   <a>Map</a>, with value-level counterparts.
--   
--   Described in the paper "Embedding effect systems in Haskell" by
--   Dominic Orchard and Tomas Petricek
--   <a>http://www.cl.cam.ac.uk/~dao29/publ/haskell14-effects.pdf</a>
--   (Haskell Symposium, 2014). This version now uses Quicksort to
--   normalise the representation.
--   
--   Here is a brief example for finite maps:
--   
--   <pre>
--   import Data.Type.Map
--   
--   -- Specify how to combine duplicate key-value pairs for Int values
--   type instance Combine Int Int = Int
--   instance Combinable Int Int where
--       combine x y = x + y
--   
--   foo :: Map '["x" :-&gt; Int, "z" :-&gt; Bool, "w" :-&gt; Int]
--   foo = Ext (Var :: (Var "x")) 2
--       $ Ext (Var :: (Var "z")) True
--       $ Ext (Var :: (Var "w")) 5
--       $ Empty
--   
--   bar :: Map '["y" :-&gt; Int, "w" :-&gt; Int]
--   bar = Ext (Var :: (Var "y")) 3
--       $ Ext (Var :: (Var "w")) 1
--       $ Empty
--   
--   -- foobar :: Map '["w" :-&gt; Int, "x" :-&gt; Int, "y" :-&gt; Int, "z" :-&gt; Bool]
--   foobar = foo `union` bar
--   </pre>
--   
--   The <a>Map</a> type for <a>foobar</a> here shows the normalised form
--   (sorted with no duplicates). The type signatures is commented out as
--   it can be infered. Running the example we get:
--   
--   <pre>
--   &gt;&gt;&gt; foobar
--   {w :-&gt; 6, x :-&gt; 2, y :-&gt; 3, z :-&gt; True}
--   </pre>
--   
--   Thus, we see that the values for "w" are added together. For sets,
--   here is an example:
--   
--   <pre>
--   import GHC.TypeLits
--   import Data.Type.Set
--   type instance Cmp (Natural n) (Natural m) = CmpNat n m
--   
--   data Natural (a :: Nat) where
--     Z :: Natural 0
--     S :: Natural n -&gt; Natural (n + 1)
--   
--   -- foo :: Set '[Natural 0, Natural 1, Natural 3]
--   foo = asSet $ Ext (S Z) (Ext (S (S (S Z))) (Ext Z Empty))
--   
--   -- bar :: Set '[Natural 1, Natural 2]
--   bar = asSet $ Ext (S (S Z)) (Ext (S Z) (Ext (S Z) Empty))
--   
--   -- foobar :: Set '[Natural 0, Natural 1, Natural 2, Natural 3]
--   foobar = foo `union` bar
--   </pre>
--   
--   Note the types here are all inferred.
@package type-level-sets
@version 0.8.9.0

module Data.Type.Set
data Set (n :: [k])
[Empty] :: Set '[]
[Ext] :: e -> Set s -> Set (e : s)

-- | Union of sets
type Union s t = Nub (Sort (s :++ t))
type Unionable s t = (Sortable (s :++ t), Nubable (Sort (s :++ t)))
union :: Unionable s t => Set s -> Set t -> Set (Union s t)
quicksort :: Sortable xs => Set xs -> Set (Sort xs)
append :: Set s -> Set t -> Set (s :++ t)

-- | Type-level quick sort for normalising the representation of sets
type family Sort (xs :: [k]) :: [k]

-- | Value-level quick sort that respects the type-level ordering
class Sortable xs

-- | List append (essentially set disjoint union)
type family (:++) (x :: [k]) (y :: [k]) :: [k]

-- | Splitting a union a set, given the sets we want to split it into
class Split s t st
split :: Split s t st => Set st -> (Set s, Set t)

-- | Open-family for the ordering operation in the sort
type family Cmp (a :: k) (b :: k) :: Ordering
type family Filter (f :: Flag) (p :: k) (xs :: [k]) :: [k]
data Flag
FMin :: Flag
FMax :: Flag

-- | Remove duplicates from a sorted list
type family Nub t

-- | Value-level counterpart to the type-level <a>Nub</a> Note: the
--   value-level case for equal types is not define here, but should be
--   given per-application, e.g., custom <tt>merging</tt> behaviour may be
--   required
class Nubable t
nub :: Nubable t => Set t -> Set (Nub t)

-- | At the type level, normalise the list form to the set form
type AsSet s = Nub (Sort s)

-- | At the value level, noramlise the list form to the set form
asSet :: (Sortable s, Nubable (Sort s)) => Set s -> Set (AsSet s)

-- | Predicate to check if in the set form
type IsSet s = (s ~ Nub (Sort s))

-- | Construct a subsetset <tt>s</tt> from a superset <tt>t</tt>
class Subset s t
subset :: Subset s t => Set t -> Set s
type family Delete elem set
data Proxy (p :: k)
Proxy :: Proxy
remove :: Remove s t => Set s -> Proxy t -> Set (s :\ t)
class Remove s t

-- | Delete elements from a set
type family (m :: [k]) :\ (x :: k) :: [k]

-- | Membership of an element in a set, with an acommanying value-level
--   function that returns a bool
class Member a s
member :: Member a s => Proxy a -> Set s -> Bool
type NonMember a s = MemberP a s ~ False
type family MemberP a s :: Bool
instance forall k (a :: k) (s :: [k]). Data.Type.Set.Member a (a : s)
instance forall k1 k2 (a :: k2) (s :: [k1]) (b :: k1). Data.Type.Set.Member a s => Data.Type.Set.Member a (b : s)
instance Data.Type.Set.Sortable '[]
instance (Data.Type.Set.Sortable (Data.Type.Set.Filter 'Data.Type.Set.FMin p xs), Data.Type.Set.Sortable (Data.Type.Set.Filter 'Data.Type.Set.FMax p xs), Data.Type.Set.FilterV 'Data.Type.Set.FMin p xs, Data.Type.Set.FilterV 'Data.Type.Set.FMax p xs) => Data.Type.Set.Sortable (p : xs)
instance Data.Type.Set.FilterV f p '[]
instance (Data.Type.Set.Conder (Data.Type.Set.Cmp x p Data.Type.Equality.== 'GHC.Types.LT), Data.Type.Set.FilterV 'Data.Type.Set.FMin p xs) => Data.Type.Set.FilterV 'Data.Type.Set.FMin p (x : xs)
instance (Data.Type.Set.Conder ((Data.Type.Set.Cmp x p Data.Type.Equality.== 'GHC.Types.GT) Data.Type.Bool.|| (Data.Type.Set.Cmp x p Data.Type.Equality.== 'GHC.Types.EQ)), Data.Type.Set.FilterV 'Data.Type.Set.FMax p xs) => Data.Type.Set.FilterV 'Data.Type.Set.FMax p (x : xs)
instance Data.Type.Set.Conder 'GHC.Types.True
instance Data.Type.Set.Conder 'GHC.Types.False
instance Data.Type.Set.Subset '[] '[]
instance forall k1 k2 (s :: [k2]) (t :: [k1]) (x :: k1). Data.Type.Set.Subset s t => Data.Type.Set.Subset s (x : t)
instance forall k (s :: [k]) (t :: [k]) (x :: k). Data.Type.Set.Subset s t => Data.Type.Set.Subset (x : s) (x : t)
instance Data.Type.Set.Nubable '[]
instance forall k (e :: k). Data.Type.Set.Nubable '[e]
instance forall k (e :: k) (s :: [k]). Data.Type.Set.Nubable (e : s) => Data.Type.Set.Nubable (e : e : s)
instance forall k (e :: k) (f :: k) (s :: [k]). (Data.Type.Set.Nub (e : f : s) Data.Type.Equality.~ (e : Data.Type.Set.Nub (f : s)), Data.Type.Set.Nubable (f : s)) => Data.Type.Set.Nubable (e : f : s)
instance Data.Type.Set.Split '[] '[] '[]
instance forall k (s :: [k]) (t :: [k]) (st :: [k]) (x :: k). Data.Type.Set.Split s t st => Data.Type.Set.Split (x : s) (x : t) (x : st)
instance forall k1 k2 (s :: [k2]) (t :: [k1]) (st :: [k2]) (x :: k2). Data.Type.Set.Split s t st => Data.Type.Set.Split (x : s) t (x : st)
instance forall k1 k2 (s :: [k2]) (t :: [k1]) (st :: [k1]) (x :: k1). Data.Type.Set.Split s t st => Data.Type.Set.Split s (x : t) (x : st)
instance forall k (t :: k). Data.Type.Set.Remove '[] t
instance forall k (xs :: [k]) (x :: k). Data.Type.Set.Remove xs x => Data.Type.Set.Remove (x : xs) x
instance forall k (y :: k) (xs :: [k]) (x :: k). (((y : xs) Data.Type.Set.:\ x) Data.Type.Equality.~ (y : (xs Data.Type.Set.:\ x)), Data.Type.Set.Remove xs x) => Data.Type.Set.Remove (y : xs) x
instance (GHC.Show.Show e, Data.Type.Set.Show' (Data.Type.Set.Set s)) => GHC.Show.Show (Data.Type.Set.Set (e : s))
instance Data.Type.Set.Show' (Data.Type.Set.Set '[])
instance (Data.Type.Set.Show' (Data.Type.Set.Set s), GHC.Show.Show e) => Data.Type.Set.Show' (Data.Type.Set.Set (e : s))
instance GHC.Show.Show (Data.Type.Set.Set '[])
instance (GHC.Classes.Eq e, GHC.Classes.Eq (Data.Type.Set.Set s)) => GHC.Classes.Eq (Data.Type.Set.Set (e : s))

module Data.Type.Map

-- | A key-value pair
data Mapping k v
(:->) :: k -> v -> Mapping k v
infixr 4 :->

-- | Union of two finite maps
type Union m n = Nub (Sort (m :++ n))
type Unionable s t = (Nubable (Sort (s :++ t)), Sortable (s :++ t))

-- | Union of two finite maps (normalising)
union :: Unionable s t => Map s -> Map t -> Map (Union s t)

-- | Pair a symbol (representing a variable) with a type
data Var (k :: Symbol)
Var :: Var

-- | A value-level heterogenously-typed Map (with type-level representation
--   in terms of lists)
data Map (n :: [Mapping Symbol *])
[Empty] :: Map '[]
[Ext] :: Var k -> v -> Map m -> Map ((k :-> v) : m)

-- | Open type family for combining values in a map (that have the same
--   key)
type family Combine (a :: v) (b :: v) :: v
class Combinable t t'
combine :: Combinable t t' => t -> t' -> Combine t t'

-- | Open-family for the ordering operation in the sort
type family Cmp (a :: k) (b :: k) :: Ordering
class Nubable t
nub :: Nubable t => Map t -> Map (Nub t)

-- | Type-level lookup of elements from a map
type family Lookup (m :: [Mapping k v]) (c :: k) :: Maybe v

-- | Membership test as type function
type family Member (c :: k) (m :: [Mapping k v]) :: Bool

-- | Delete elements from a map by key
type family (m :: [Mapping k v]) :\ (c :: k) :: [Mapping k v]

-- | Splitting a union of maps, given the maps we want to split it into
class Split s t st
split :: Split s t st => Map st -> (Map s, Map t)

-- | Membership test a type class (predicate)
class IsMember v t m

-- | Value-level lookup of elements from a map, via type class predicate
lookp :: IsMember v t m => Var v -> Map m -> t

-- | Updatability as a type class
class Updatable v t m n

-- | Update a map with <tt>m</tt> at variable <tt>v</tt> with a value of
--   type <tt>t</tt> to produce a map of type <tt>n</tt>
update :: Updatable v t m n => Map m -> Var v -> t -> Map n

-- | Predicate to check if in normalised map form
type IsMap s = (s ~ Nub (Sort s))

-- | At the type level, normalise the list form to the map form
type AsMap s = Nub (Sort s)

-- | At the value level, noramlise the list form to the map form
asMap :: (Sortable s, Nubable (Sort s)) => Map s -> Map (AsMap s)

-- | Construct a submap <tt>s</tt> from a supermap <tt>t</tt>
class Submap s t
submap :: Submap s t => Map t -> Map s
instance Data.Type.Map.Submap '[] '[]
instance Data.Type.Map.Submap s t => Data.Type.Map.Submap s (x : t)
instance Data.Type.Map.Submap s t => Data.Type.Map.Submap (x : s) (x : t)
instance Data.Type.Map.Split '[] '[] '[]
instance Data.Type.Map.Split s t st => Data.Type.Map.Split (x : s) (x : t) (x : st)
instance Data.Type.Map.Split s t st => Data.Type.Map.Split (x : s) t (x : st)
instance Data.Type.Map.Split s t st => Data.Type.Map.Split s (x : t) (x : st)
instance (Data.Type.Map.Conder (Data.Type.Set.Cmp x (k 'Data.Type.Map.:-> v) Data.Type.Equality.== 'GHC.Types.LT), Data.Type.Map.FilterV 'Data.Type.Set.FMin k v xs) => Data.Type.Map.FilterV 'Data.Type.Set.FMin k v (x : xs)
instance (Data.Type.Map.Conder ((Data.Type.Set.Cmp x (k 'Data.Type.Map.:-> v) Data.Type.Equality.== 'GHC.Types.GT) Data.Type.Bool.|| (Data.Type.Set.Cmp x (k 'Data.Type.Map.:-> v) Data.Type.Equality.== 'GHC.Types.EQ)), Data.Type.Map.FilterV 'Data.Type.Set.FMax k v xs) => Data.Type.Map.FilterV 'Data.Type.Set.FMax k v (x : xs)
instance Data.Type.Map.Conder 'GHC.Types.True
instance Data.Type.Map.Conder 'GHC.Types.False
instance Data.Type.Map.Nubable '[]
instance Data.Type.Map.Nubable '[e]
instance (Data.Type.Map.Nub (e : f : s) Data.Type.Equality.~ (e : Data.Type.Map.Nub (f : s)), Data.Type.Map.Nubable (f : s)) => Data.Type.Map.Nubable (e : f : s)
instance (Data.Type.Map.Combinable v v', Data.Type.Map.Nubable ((k 'Data.Type.Map.:-> Data.Type.Map.Combine v v') : s)) => Data.Type.Map.Nubable ((k 'Data.Type.Map.:-> v) : (k 'Data.Type.Map.:-> v') : s)
instance (Data.Type.Map.Sortable (Data.Type.Set.Filter 'Data.Type.Set.FMin (k 'Data.Type.Map.:-> v) xs), Data.Type.Map.Sortable (Data.Type.Set.Filter 'Data.Type.Set.FMax (k 'Data.Type.Map.:-> v) xs), Data.Type.Map.FilterV 'Data.Type.Set.FMin k v xs, Data.Type.Map.FilterV 'Data.Type.Set.FMax k v xs) => Data.Type.Map.Sortable ((k 'Data.Type.Map.:-> v) : xs)
instance Data.Type.Map.FilterV f k v '[]
instance Data.Type.Map.Sortable '[]
instance (GHC.TypeLits.KnownSymbol k, GHC.Show.Show v, Data.Type.Map.Show' (Data.Type.Map.Map s)) => GHC.Show.Show (Data.Type.Map.Map ((k 'Data.Type.Map.:-> v) : s))
instance Data.Type.Map.Show' (Data.Type.Map.Map '[])
instance (GHC.TypeLits.KnownSymbol k, GHC.Show.Show v, Data.Type.Map.Show' (Data.Type.Map.Map s)) => Data.Type.Map.Show' (Data.Type.Map.Map ((k 'Data.Type.Map.:-> v) : s))
instance Data.Type.Map.Updatable v t ((v 'Data.Type.Map.:-> s) : m) ((v 'Data.Type.Map.:-> t) : m)
instance Data.Type.Map.Updatable v t m n => Data.Type.Map.Updatable v t ((w 'Data.Type.Map.:-> y) : m) ((w 'Data.Type.Map.:-> y) : n)
instance Data.Type.Map.Updatable v t s ((v 'Data.Type.Map.:-> t) : s)
instance Data.Type.Map.IsMember v t ((v 'Data.Type.Map.:-> t) : m)
instance Data.Type.Map.IsMember v t m => Data.Type.Map.IsMember v t (x : m)
instance GHC.Show.Show (Data.Type.Map.Map '[])
instance GHC.Classes.Eq (Data.Type.Map.Map '[])
instance (GHC.Classes.Eq v, GHC.Classes.Eq (Data.Type.Map.Map s)) => GHC.Classes.Eq (Data.Type.Map.Map ((k 'Data.Type.Map.:-> v) : s))
instance GHC.Classes.Ord (Data.Type.Map.Map '[])
instance (GHC.Classes.Ord v, GHC.Classes.Ord (Data.Type.Map.Map s)) => GHC.Classes.Ord (Data.Type.Map.Map ((k 'Data.Type.Map.:-> v) : s))
instance GHC.TypeLits.KnownSymbol k => GHC.Show.Show (Data.Type.Map.Var k)