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


-- | Type-level sets and finite maps (with value-level counterparts and various operations)
--   
--   This package provides type-level sets (no duplicates, sorted to
--   provide a normal form) via <a>Set</a> and type-level 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)
--   
--   Here is a brief example:
--   
--   <pre>
--   import Data.Type.Map
--   
--   foo :: Set '["x" :-&gt; Int, "z" :-&gt; Int, "w" :-&gt; Int]
--   foo = Ext ((Var :: (Var "x")) :-&gt; 2) $
--           Ext ((Var :: (Var "z")) :-&gt; 4) $
--             Ext ((Var :: (Var "w")) :-&gt; 5) $
--               Empty
--   
--   bar :: Set '["y" :-&gt; Int, "w" :-&gt; Int]
--   bar = Ext ((Var :: (Var "y")) :-&gt; 3) $
--           Ext ((Var :: (Var "w")) :-&gt; 1) $
--             Empty
--   
--   -- foobar :: Set '["w" :-&gt; Int, "x" :-&gt; Int, "y" :-&gt; Int, "z" :-&gt; Int]
--   foobar = foo `union` bar
--   </pre>
--   
--   The <a>Set</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
--   [(Var :-&gt; 1), (Var :-&gt; 2), (Var :-&gt; 3), (Var :-&gt; 4)]
--   </pre>
--   
--   Thus, we see that the first value paired with the "w" variable is
--   dropped.
@package type-level-sets
@version 0.6

module Data.Type.Set
data Set (n :: [*])
[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

-- | Value-level quick sort that respects the type-level ordering
class Sortable xs
quicksort :: Sortable xs => Set xs -> Set (Sort xs)

-- | List append (essentially set disjoint union)

-- | 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
data Flag
FMin :: Flag
FMax :: Flag

-- | Remove duplicates from a sorted list

-- | 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
data Proxy (p :: k)
Proxy :: Proxy
instance GHC.Show.Show (Data.Type.Set.Set '[])
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 Data.Type.Set.Split '[] '[] '[]
instance Data.Type.Set.Split s t st => Data.Type.Set.Split (x : s) (x : t) (x : st)
instance Data.Type.Set.Split s t st => Data.Type.Set.Split (x : s) t (x : st)
instance Data.Type.Set.Split s t st => Data.Type.Set.Split s (x : t) (x : st)
instance Data.Type.Set.Nubable '[]
instance Data.Type.Set.Nubable '[e]
instance Data.Type.Set.Nubable (e : s) => Data.Type.Set.Nubable (e : e : s)
instance (Data.Type.Set.Nub (e : f : s) ~ (e : Data.Type.Set.Nub (f : s)), Data.Type.Set.Nubable (f : s)) => Data.Type.Set.Nubable (e : f : s)
instance Data.Type.Set.Subset '[] '[]
instance Data.Type.Set.Subset '[] (x : t)
instance Data.Type.Set.Subset s t => Data.Type.Set.Subset (x : s) (x : t)
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

module Data.Type.Map

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

-- | 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
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)
class Combinable t t'
combine :: Combinable t t' => t -> t' -> Combine t t'

-- | Open-family for the ordering operation in the sort

-- | Lookup elements from a map

-- | Membership test

-- | Delete elements from a map by key
instance GHC.TypeLits.KnownSymbol k => GHC.Show.Show (Data.Type.Map.Var k)
instance GHC.Show.Show (Data.Type.Map.Map '[])
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.Sortable '[]
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.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.Nubable '[]
instance Data.Type.Map.Nubable '[e]
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.Nub (e : f : s) ~ (e : Data.Type.Map.Nub (f : s)), Data.Type.Map.Nubable (f : s)) => Data.Type.Map.Nubable (e : f : s)
instance Data.Type.Map.Conder 'GHC.Types.True
instance Data.Type.Map.Conder 'GHC.Types.False