-- 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
--   </pre>
--   
--   w :-&gt; 6, x :-&gt; 2, y :-&gt; 3, z :-&gt; True
--   
--   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.7

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)
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 s t => Data.Type.Set.Subset s (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
class Nubable t
nub :: Nubable t => Map t -> Map (Nub t)

-- | Lookup elements from a map

-- | Membership test

-- | Delete elements from a map by key

-- | 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)

-- | 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 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.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.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.Conder 'GHC.Types.True
instance Data.Type.Map.Conder 'GHC.Types.False
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.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)