Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
- In addition to
Map
andSet
, types interpretable as maps and sets. - Classes supporting abstract constructors of Set Algebra Expressions. These show up in the types of overloaded functions.
- Types implementing a deep embedding of set algebra expressions
- Operators to build maps and sets, useable as Set Algebra Expressions
- Miscellaneous operators, including smart constructors for
List
, whose constructors are hidden.
Operations for manipulating sets and maps using mathematicial operators. Concrete types that can be
interpreted as sets and maps are made instances of the Basic
class. In order to make sets and maps
behave uniformly, an instance (Basic f)
implies f
is a binary type constructor. For types interpreted as
maps, the type
(f k v)
means that k
is the type of the map's key, and v
is the type of map's value. For types
interpreted as sets, the value is always the unit type: (). The binary GADT Sett
links to the
usual Set
type. Its constructor has the following type Sett :: Set k -> Sett k ()
, programmers can
use similar strategies to interpret other types as sets. Predefined instances of Basic include Map
,
Set
, List
, and Single
. Programmers can add Basic
instances for their own types as well.
A typical set algebra expression (involving range restriction, (▷
), here) looks like (eval (x ▷ y))
.
Where x
and y
are program variables or expressions, the operator (▷
) builds an Exp
tree, and
eval
simplifys the tree, and then evaluates the simplfied tree to get the result.
Here is the actual type of the range restrict operator.
(▷) :: (Ord k, Iter g, Ord v, HasExp s1 (f k v), HasExp s2 (g v ())) => s1 -> s2 -> Exp (f k v)
As the type indicates, in order to support simplifcation and evaluation the types of the
operands to (▷
) must be instances of several classes. Possible classes include Basic
,
HasExp
, Iter
, and Embed
.
(Basic f)
meaning(f k v)
must be interpreted as a map or set, with two type parametersk
andv
.(HasExp t (f k v))
meaning a value of typet
can be lifted to an expression of type(Exp (f k v))
, where(Basic f)
.(Iter f)
meaning theBasic
type constructorf
supports certain (usually fast) operations, that can be combined.(Embed concrete f)
meaning the typesconcrete
and(f k v)
form an isomorphism.
Available operands to create set algebra expressions are dom
, rng
, dexclude
, (⋪)
, drestrict
, (◁)
,
rexclude
, (⋫)
, rrestrict
, (▷)
,
unionright
, (⨃)
, unionleft
,(∪)
, unionplus
, (∪+)
,singleton
, setSingleton
,
intersect
, (∩)
, subset
, (⊆)
, keyeq
, (≍)
,
(∈)
, (∉)
, setdiff
, (➖)
.
The key abstraction that makes set algebra work is the self typed GADT: (Exp t)
, that defines a tree that
represents a deep embedding of all set algebra expressions representing maps or sets of type t
.
Exp
is a typed symbolic representation of queries we may ask. It allows us to introspect a query.
The strategy is to
- Define Exp so all queries can be represented.
- Define smart constructors that "parse" the surface syntax, and build a typed Exp
- Write an evaluate function: eval:: Exp t -> t
- "eval" can introspect the code and apply efficient domain and type specific translations
- Use the (Iter f) class to evaluate some Exp that can benefit from its efficient nature.
Basically, if the compiler can infer concrete type for the operands of operators then all the class instances are automatically solved. If you get an error involving a class, then it is most probably the case that the type of the operands cannot be properly inferred.
Synopsis
- data List k v
- data Single k v where
- class Basic f where
- class Iter f where
- nxt ∷ f a b → Collect (a, b, f a b)
- lub ∷ Ord k ⇒ k → f k b → Collect (k, b, f k b)
- hasNxt ∷ f a b → Maybe (a, b, f a b)
- hasLub ∷ Ord k ⇒ k → f k b → Maybe (k, b, f k b)
- haskey ∷ Ord key ⇒ key → f key b → Bool
- isnull ∷ f k v → Bool
- lookup ∷ Ord key ⇒ key → f key rng → Maybe rng
- element ∷ Ord k ⇒ k → f k v → Collect ()
- class HasExp s t | s → t where
- class Embed concrete base | concrete → base where
- data BaseRep f k v where
- data Exp t where
- eval ∷ Embed s t ⇒ Exp t → s
- dom ∷ (Ord k, HasExp s (f k v)) ⇒ s → Exp (Sett k ())
- rng ∷ (Ord k, Ord v) ⇒ HasExp s (f k v) ⇒ s → Exp (Sett v ())
- dexclude ∷ (Ord k, Iter g, HasExp s1 (g k ()), HasExp s2 (f k v)) ⇒ s1 → s2 → Exp (f k v)
- drestrict ∷ (Ord k, HasExp s1 (Sett k ()), HasExp s2 (f k v)) ⇒ s1 → s2 → Exp (f k v)
- rexclude ∷ (Ord k, Iter g, Ord v, HasExp s1 (f k v), HasExp s2 (g v ())) ⇒ s1 → s2 → Exp (f k v)
- rrestrict ∷ (Ord k, Iter g, Ord v, HasExp s1 (f k v), HasExp s2 (g v ())) ⇒ s1 → s2 → Exp (f k v)
- unionleft ∷ (Show k, Show v, Ord k, HasExp s1 (f k v), HasExp s2 (g k v)) ⇒ s1 → s2 → Exp (f k v)
- unionright ∷ (Ord k, HasExp s1 (f k v), HasExp s2 (g k v)) ⇒ s1 → s2 → Exp (f k v)
- unionplus ∷ (Ord k, Monoid n, HasExp s1 (f k n), HasExp s2 (g k n)) ⇒ s1 → s2 → Exp (f k n)
- singleton ∷ Ord k ⇒ k → v → Exp (Single k v)
- setSingleton ∷ Ord k ⇒ k → Exp (Single k ())
- intersect ∷ (Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) ⇒ s1 → s2 → Exp (Sett k ())
- subset ∷ (Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) ⇒ s1 → s2 → Exp Bool
- keyeq ∷ (Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) ⇒ s1 → s2 → Exp Bool
- (◁) ∷ (Ord k, HasExp s1 (Sett k ()), HasExp s2 (f k v)) ⇒ s1 → s2 → Exp (f k v)
- (⋪) ∷ (Ord k, Iter g, HasExp s1 (g k ()), HasExp s2 (f k v)) ⇒ s1 → s2 → Exp (f k v)
- (▷) ∷ (Ord k, Iter g, Ord v, HasExp s1 (f k v), HasExp s2 (g v ())) ⇒ s1 → s2 → Exp (f k v)
- (⋫) ∷ (Ord k, Iter g, Ord v, HasExp s1 (f k v), HasExp s2 (g v ())) ⇒ s1 → s2 → Exp (f k v)
- (∈) ∷ (Show k, Ord k, Iter g, HasExp s (g k ())) ⇒ k → s → Exp Bool
- (∉) ∷ (Show k, Ord k, Iter g, HasExp s (g k ())) ⇒ k → s → Exp Bool
- (∪) ∷ (Show k, Show v, Ord k, HasExp s1 (f k v), HasExp s2 (g k v)) ⇒ s1 → s2 → Exp (f k v)
- (⨃) ∷ (Ord k, HasExp s1 (f k v), HasExp s2 (g k v)) ⇒ s1 → s2 → Exp (f k v)
- (∪+) ∷ (Ord k, Monoid n, HasExp s1 (f k n), HasExp s2 (g k n)) ⇒ s1 → s2 → Exp (f k n)
- (∩) ∷ (Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) ⇒ s1 → s2 → Exp (Sett k ())
- (⊆) ∷ (Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) ⇒ s1 → s2 → Exp Bool
- (≍) ∷ (Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) ⇒ s1 → s2 → Exp Bool
- (<|) ∷ (Ord k, HasExp s1 (Sett k ()), HasExp s2 (f k v)) ⇒ s1 → s2 → Exp (f k v)
- (|>) ∷ (Ord k, Iter g, Ord v, HasExp s1 (f k v), HasExp s2 (g v ())) ⇒ s1 → s2 → Exp (f k v)
- (➖) ∷ (Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) ⇒ s1 → s2 → Exp (f k v)
- keysEqual ∷ Ord k ⇒ Map k v1 → Map k v2 → Bool
- setdiff ∷ (Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) ⇒ s1 → s2 → Exp (f k v)
- materialize ∷ Ord k ⇒ BaseRep f k v → Collect (k, v) → f k v
- fromList ∷ Ord k ⇒ BaseRep f k v → (v → v → v) → [(k, v)] → f k v
In addition to Map
and Set
, types interpretable as maps and sets.
Maps stored as lists. Sorted [(key,value)] pairs, with no duplicate keys.
The constructor for List is hidden, since it requires some invariants. Use fromPairs
to build an initial List.
Instances
Basic List Source # | |
Iter List Source # | |
Defined in Control.Iterate.BaseTypes nxt ∷ List a b → Collect (a, b, List a b) Source # lub ∷ Ord k ⇒ k → List k b → Collect (k, b, List k b) Source # hasNxt ∷ List a b → Maybe (a, b, List a b) Source # hasLub ∷ Ord k ⇒ k → List k b → Maybe (k, b, List k b) Source # haskey ∷ Ord key ⇒ key → List key b → Bool Source # isnull ∷ List k v → Bool Source # | |
Ord k ⇒ Embed [(k, v)] (List k v) Source # | |
Ord k ⇒ HasExp [(k, v)] (List k v) Source # | |
(Show k, Show v) ⇒ Show (List k v) Source # | |
(Eq k, Eq v) ⇒ Eq (List k v) Source # | |
data Single k v where Source #
Maps and sets with zero or a single pair. Iteration is trivial. Succeeds at most once.
Instances
Basic Single Source # | |
Defined in Control.Iterate.BaseTypes | |
Iter Single Source # | |
Defined in Control.Iterate.BaseTypes nxt ∷ Single a b → Collect (a, b, Single a b) Source # lub ∷ Ord k ⇒ k → Single k b → Collect (k, b, Single k b) Source # hasNxt ∷ Single a b → Maybe (a, b, Single a b) Source # hasLub ∷ Ord k ⇒ k → Single k b → Maybe (k, b, Single k b) Source # haskey ∷ Ord key ⇒ key → Single key b → Bool Source # isnull ∷ Single k v → Bool Source # lookup ∷ Ord key ⇒ key → Single key rng → Maybe rng Source # | |
(Show k, Show v) ⇒ Show (Single k v) Source # | |
(Eq k, Eq v) ⇒ Eq (Single k v) Source # | |
Ord k ⇒ HasQuery (Single k v) k v Source # | |
Embed (Single k v) (Single k v) Source # | |
Ord k ⇒ HasExp (Single k v) (Single k v) Source # | |
Classes supporting abstract constructors of Set Algebra Expressions. These show up in the types of overloaded functions.
In order to build typed Exp
(which are a typed deep embedding) of map and set operations, we need to know
what kind of basic types can be used this way. Every Basic type has a few operations
for creating one from a list, for adding and removing key-value pairs, looking up a value given a key.
Instances of this algebra are functional in that every key has exactly one value associated with it.
addpair ∷ Ord k ⇒ k → v → f k v → f k v Source #
in addpair the new value always prevails, to make a choice use addkv
which has a combining function that allows choice.
addkv ∷ Ord k ⇒ (k, v) → f k v → (v → v → v) → f k v Source #
use ( old new -> old) if you want the v in (f k v) to prevail, and use ( old new -> new) if you want the v in (k,v) to prevail
removekey ∷ Ord k ⇒ k → f k v → f k v Source #
remove the pair with key k
, if it is there.
domain ∷ Ord k ⇒ f k v → Set k Source #
the set of keys
range ∷ Ord v ⇒ f k v → Set v Source #
the set of values.
The Set algebra include types that encode finite sets and maps of some type. They
have a finite domain, and for each domain element they pair a single range
element (unit for sets). We are interested in those finite maps that can iterate their
pairs in ascending domain order. The operations are: nxt
and lub
.
lub can skip over many items in sub-linear time, it can make things really fast.
Many finite maps can support a support lub operation in sub-linear time. Some examples:
Balanced binary trees, Arrays (using binary search), Tries, etc. There are basic and compound
Iter instances. Compound types include components with types that have Iter instances.
nxt ∷ f a b → Collect (a, b, f a b) Source #
lub ∷ Ord k ⇒ k → f k b → Collect (k, b, f k b) Source #
hasNxt ∷ f a b → Maybe (a, b, f a b) Source #
The next few methods can all be defined via nxt and lub, but for base types there often exist much more efficent means, so the default definitions should be overwritten for such basic types. For compound types with Guards, these are often the only way to define them.
hasLub ∷ Ord k ⇒ k → f k b → Maybe (k, b, f k b) Source #
haskey ∷ Ord key ⇒ key → f key b → Bool Source #
isnull ∷ f k v → Bool Source #
Instances
class HasExp s t | s → t where Source #
Basic types are those that can be tranformed into Exp.
The HasExp class, encodes how to lift a Basic type into an Exp.
The function toExp
will build a typed Exp for that Basic type.
This will be really usefull in the smart constructors.
class Embed concrete base | concrete → base where Source #
Every iterable type type forms an isomorphism with some Base type. For most
Base types the isomorphism is the identity in both directions, but for some,
like List and Sett, the embeddings are not the trivial identities because the
concrete types are not binary type constructors. The Embed class also allows
us to add newtypes
which encode some Base type to the system.
Types implementing a deep embedding of set algebra expressions
data BaseRep f k v where Source #
BaseRep witnesses Basic types. I.e. those types that are instances of both Basic and Iter. Pattern matching against a constructor of type BaseRep, determines which base type. For example data Tag f k v = Tag (BaseRep f k v) (f k v) case Tag MapR x -> -- here we know x :: Map.Map k v
The self typed GADT: Exp, that encodes the shape of Set expressions. A deep embedding. Exp is a typed Symbolic representation of queries we may ask. It allows us to introspect a query The strategy is to
- Define Exp so all queries can be represented.
- Define smart constructors that "parse" the surface syntax, and build a typed Exp
- Write an evaluate function: eval:: Exp t -> t
- "eval" can introspect the code and apply efficient domain and type specific translations
- Use the (Iter f) class to evaluate some Exp that can benefit from its efficient nature.
Instances
Operators to build maps and sets, useable as Set Algebra Expressions
dom ∷ (Ord k, HasExp s (f k v)) ⇒ s → Exp (Sett k ()) Source #
domain of a map or element type of a set.
rng ∷ (Ord k, Ord v) ⇒ HasExp s (f k v) ⇒ s → Exp (Sett v ()) Source #
range of a map or () for a set.
dexclude ∷ (Ord k, Iter g, HasExp s1 (g k ()), HasExp s2 (f k v)) ⇒ s1 → s2 → Exp (f k v) Source #
domain exclude
drestrict ∷ (Ord k, HasExp s1 (Sett k ()), HasExp s2 (f k v)) ⇒ s1 → s2 → Exp (f k v) Source #
domain restrict.
rexclude ∷ (Ord k, Iter g, Ord v, HasExp s1 (f k v), HasExp s2 (g v ())) ⇒ s1 → s2 → Exp (f k v) Source #
range exclude
rrestrict ∷ (Ord k, Iter g, Ord v, HasExp s1 (f k v), HasExp s2 (g v ())) ⇒ s1 → s2 → Exp (f k v) Source #
range restrict
unionleft ∷ (Show k, Show v, Ord k, HasExp s1 (f k v), HasExp s2 (g k v)) ⇒ s1 → s2 → Exp (f k v) Source #
union two maps or sets. In the case of a map, keep the pair from the left, if the two have common keys.
unionright ∷ (Ord k, HasExp s1 (f k v), HasExp s2 (g k v)) ⇒ s1 → s2 → Exp (f k v) Source #
union two maps or sets. In the case of a map, keep the pair from the right, if the two have common keys.
unionplus ∷ (Ord k, Monoid n, HasExp s1 (f k n), HasExp s2 (g k n)) ⇒ s1 → s2 → Exp (f k n) Source #
union two maps or sets. In the case of a map, combine values with monoid (<>), if the two have common keys.
intersect ∷ (Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) ⇒ s1 → s2 → Exp (Sett k ()) Source #
intersect two sets, or the intersection of the domain of two maps.
subset ∷ (Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) ⇒ s1 → s2 → Exp Bool Source #
(subset x y)
. is the domain of x
a subset of the domain of y
.
keyeq ∷ (Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) ⇒ s1 → s2 → Exp Bool Source #
Do two maps (or sets) have exactly the same domain.
(◁) ∷ (Ord k, HasExp s1 (Sett k ()), HasExp s2 (f k v)) ⇒ s1 → s2 → Exp (f k v) Source #
domain restrict.
(⋪) ∷ (Ord k, Iter g, HasExp s1 (g k ()), HasExp s2 (f k v)) ⇒ s1 → s2 → Exp (f k v) Source #
domain exclude
(▷) ∷ (Ord k, Iter g, Ord v, HasExp s1 (f k v), HasExp s2 (g v ())) ⇒ s1 → s2 → Exp (f k v) Source #
range restrict
(⋫) ∷ (Ord k, Iter g, Ord v, HasExp s1 (f k v), HasExp s2 (g v ())) ⇒ s1 → s2 → Exp (f k v) Source #
range exclude
(∉) ∷ (Show k, Ord k, Iter g, HasExp s (g k ())) ⇒ k → s → Exp Bool Source #
not an element of the domain
(∪) ∷ (Show k, Show v, Ord k, HasExp s1 (f k v), HasExp s2 (g k v)) ⇒ s1 → s2 → Exp (f k v) Source #
union two maps or sets. In the case of a map, keep the pair from the left, if the two have common keys.
(⨃) ∷ (Ord k, HasExp s1 (f k v), HasExp s2 (g k v)) ⇒ s1 → s2 → Exp (f k v) Source #
union two maps or sets. In the case of a map, keep the pair from the right, if the two have common keys.
(∪+) ∷ (Ord k, Monoid n, HasExp s1 (f k n), HasExp s2 (g k n)) ⇒ s1 → s2 → Exp (f k n) Source #
union two maps or sets. In the case of a map, combine values with monoid (<>), if the two have common keys.
(∩) ∷ (Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) ⇒ s1 → s2 → Exp (Sett k ()) Source #
intersect two sets, or the intersection of the domain of two maps.
(⊆) ∷ (Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) ⇒ s1 → s2 → Exp Bool Source #
(subset x y)
. is the domain of x
a subset of the domain of y
.
(≍) ∷ (Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) ⇒ s1 → s2 → Exp Bool Source #
Do two maps (or sets) have exactly the same domain.
(<|) ∷ (Ord k, HasExp s1 (Sett k ()), HasExp s2 (f k v)) ⇒ s1 → s2 → Exp (f k v) Source #
domain restrict.
(|>) ∷ (Ord k, Iter g, Ord v, HasExp s1 (f k v), HasExp s2 (g v ())) ⇒ s1 → s2 → Exp (f k v) Source #
range restrict
(➖) ∷ (Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) ⇒ s1 → s2 → Exp (f k v) Source #
(x ➖ y)
Everything in x
except for those pairs in x
where the domain of x
is an element of the domain of y
.
setdiff ∷ (Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) ⇒ s1 → s2 → Exp (f k v) Source #
(x ➖ y)
Everything in x
except for those pairs in x
where the domain of x
is an element of the domain of y
.
Miscellaneous operators, including smart constructors for List
, whose constructors are hidden.
materialize ∷ Ord k ⇒ BaseRep f k v → Collect (k, v) → f k v Source #
A witness (BaseRep) can be used to materialize a (Collect k v) into the type witnessed by the BaseRep. Recall a (Collect k v) has no intrinsic type (it is just an ABSTRACT sequence of tuples), so the witness describes how to turn them into the chosen datatype. Note that materialize is meant to be applied to a collection built by iterating over a Query. This produces the keys in ascending order, with no duplicate keys. So we do not need to specify how to merge duplicate values.
fromList ∷ Ord k ⇒ BaseRep f k v → (v → v → v) → [(k, v)] → f k v Source #
Turn a list of pairs into any Basic
type. The first argument is a BaseRep
which
chooses what Base type to construct.
The combine function comb = (\ earlier later -> later) will let values
later in the list override ones earlier in the list, and comb =
(\ earlier later -> earlier) will keep the value that appears first in the list