Copyright  Copyright (c) 2016 the Hakaru team 

License  BSD3 
Maintainer  wren@community.haskell.org 
Stability  experimental 
Portability  GHConly 
Safe Haskell  None 
Language  Haskell2010 
An implementation of variables, for use with Language.Hakaru.Syntax.ABT.
 data Variable a = Variable {}
 varEq :: (Show1 (Sing :: k > *), JmEq1 (Sing :: k > *)) => Variable (a :: k) > Variable (b :: k) > Maybe (TypeEq a b)
 data VarEqTypeError where
 VarEqTypeError :: (Show1 (Sing :: k > *), JmEq1 (Sing :: k > *)) => !(Variable (a :: k)) > !(Variable (b :: k)) > VarEqTypeError
 type KindOf a = (KProxy :: KProxy k)
 data SomeVariable kproxy = SomeVariable !(Variable (a :: k))
 newtype VarSet kproxy = VarSet {
 unVarSet :: IntMap (SomeVariable kproxy)
 emptyVarSet :: VarSet kproxy
 singletonVarSet :: Variable a > VarSet (KindOf a)
 fromVarSet :: VarSet kproxy > [SomeVariable kproxy]
 toVarSet :: [SomeVariable kproxy] > VarSet kproxy
 toVarSet1 :: List1 Variable (xs :: [k]) > VarSet (kproxy :: KProxy k)
 insertVarSet :: Variable a > VarSet (KindOf a) > VarSet (KindOf a)
 deleteVarSet :: Variable a > VarSet (KindOf a) > VarSet (KindOf a)
 memberVarSet :: (Show1 (Sing :: k > *), JmEq1 (Sing :: k > *)) => Variable (a :: k) > VarSet (kproxy :: KProxy k) > Bool
 nextVarID :: VarSet kproxy > Nat
 data Assoc ast = Assoc !(Variable a) !(ast a)
 newtype Assocs ast = Assocs {}
 emptyAssocs :: Assocs abt
 singletonAssocs :: Variable a > f a > Assocs f
 fromAssocs :: Assocs ast > [Assoc ast]
 toAssocs :: [Assoc ast] > Assocs ast
 toAssocs1 :: List1 Variable xs > List1 ast xs > Assocs ast
 insertAssoc :: Assoc ast > Assocs ast > Assocs ast
 insertAssocs :: Assocs ast > Assocs ast > Assocs ast
 lookupAssoc :: (Show1 (Sing :: k > *), JmEq1 (Sing :: k > *)) => Variable (a :: k) > Assocs ast > Maybe (ast a)
 adjustAssoc :: Variable (a :: k) > (Assoc ast > Assoc ast) > Assocs ast > Assocs ast
 mapAssocs :: (Assoc ast1 > Assoc ast2) > Assocs ast1 > Assocs ast2
Our basic notion of variables.
A variable is a triple of a unique identifier (varID
), a
hint for how to display things to humans (varHint
), and a type
(varType
). Notably, the hint is only used for display purposes,
and the type is only used for typing purposes; thus, the Eq
and Ord
instances only look at the unique identifier, completely
ignoring the other two components. However, the varEq
function
does take the type into consideration (but still ignores the
hint).
N.B., the unique identifier is lazy so that we can tietheknot
in binder
.
varEq :: (Show1 (Sing :: k > *), JmEq1 (Sing :: k > *)) => Variable (a :: k) > Variable (b :: k) > Maybe (TypeEq a b) Source #
Compare to variables at possiblydifferent types. If the
variables are "equal", then they must in fact have the same
type. N.B., it is not entirely specified what this function
means when two variables have the same varID
but different
varType
. However, so long as we use this function everywhere,
at least we'll be consistent.
Possible interpretations:
 We could assume that when the
varType
s do not match the variables are not equal. Upside: we can statically guarantee that every variable is "welltyped" (by fiat). Downside: every type has its own variable namespace, which is very confusing. Also, theOrd SomeVariable
instance will be really difficult to get right.  We could require that whenever two
varID
s match, theirvarType
s must also match. Upside: a single variable namespace. Downside: if the types do not in fact match (e.g., the preprocessing step for ensuring variable uniqueness is buggy), then we must throw (or return) anVarEqTypeError
exception.  We could assert that whenever two
varID
s match, theirvarType
s must also match. Upsides: we get a single variable namespace, and we get O(1) equality checking. Downsides: if the types do not in fact match, we'll probably segfault.
Whichever interpretation we choose, we must make sure that typing contexts, binding environments, and so on all behave consistently.
data VarEqTypeError where Source #
An exception type for if we need to throw an error when two
variables do not have an equal varType
. This is mainly used
when varEq
chooses the second interpretation.
VarEqTypeError :: (Show1 (Sing :: k > *), JmEq1 (Sing :: k > *)) => !(Variable (a :: k)) > !(Variable (b :: k)) > VarEqTypeError 
Variables with existentially quantified types
type KindOf a = (KProxy :: KProxy k) Source #
Convenient synonym to refer to the kind of a type variable:
type KindOf (a :: k) = ('KProxy :: KProxy k)
data SomeVariable kproxy Source #
Hide an existentially quantified parameter to Variable
.
Because the Variable
type is polykinded, we need to be careful
not to erase too much type/kind information. Thus, we parameterize
the SomeVariable
type by the kind of the type we existentially
quantify over. This is necessary for giving Eq
and Ord
instances since we can only compare variables whose types live
in the same kind.
N.B., the Ord
instance assumes that varEq
uses either the
second or third interpretation. If varEq
uses the first
interpretation then, the Eq
instance (which uses varEq
) will
be inconsistent with the Ord
instance!
SomeVariable !(Variable (a :: k)) 
Some helper types for "heaps", "environments", etc
Typing environments; aka: sets of (typed) variables
newtype VarSet kproxy Source #
A set of (typed) variables.
VarSet  

emptyVarSet :: VarSet kproxy Source #
fromVarSet :: VarSet kproxy > [SomeVariable kproxy] Source #
toVarSet :: [SomeVariable kproxy] > VarSet kproxy Source #
Convert a list of variables into a variable set.
In the event that multiple variables have conflicting varID
,
the latter variable will be kept. This generally won't matter
because we're treating the list as a set. In the cases where
it would matter, chances are you're going to encounter a
VarEqTypeError
sooner or later anyways.
toVarSet1 :: List1 Variable (xs :: [k]) > VarSet (kproxy :: KProxy k) Source #
Convert a list of variables into a variable set.
In the event that multiple variables have conflicting varID
,
the latter variable will be kept. This generally won't matter
because we're treating the list as a set. In the cases where
it would matter, chances are you're going to encounter a
VarEqTypeError
sooner or later anyways.
memberVarSet :: (Show1 (Sing :: k > *), JmEq1 (Sing :: k > *)) => Variable (a :: k) > VarSet (kproxy :: KProxy k) > Bool Source #
nextVarID :: VarSet kproxy > Nat Source #
Return the successor of the largest varID
of all the variables
in the set. Thus, we return zero for the empty set and nonzero
for nonempty sets.
Substitutions; aka: maps from variables to their definitions
A pair of variable and term, both of the same Hakaru type.
A set of variable/term associations.
N.B., the current implementation assumes varEq
uses either the
second or third interpretations; that is, it is impossible to
have a single varID
be shared by multiple variables (i.e., at
different types). If you really want the first interpretation,
then the implementation must be updated.
emptyAssocs :: Assocs abt Source #
The empty set of associations.
singletonAssocs :: Variable a > f a > Assocs f Source #
A single association.
fromAssocs :: Assocs ast > [Assoc ast] Source #
Convert an association list into a list of associations.
toAssocs :: [Assoc ast] > Assocs ast Source #
Convert a list of associations into an association list. In the event of conflict, later associations override earlier ones.
toAssocs1 :: List1 Variable xs > List1 ast xs > Assocs ast Source #
Convert an unzipped list of curried associations into an association list. In the event of conflict, later associations override earlier ones.
insertAssoc :: Assoc ast > Assocs ast > Assocs ast Source #
Add an association to the set of associations.
HACK: if the variable is already associated with some term then
we throw an error! In the future it'd be better to take some
sort of continuation to decide between (a) replacing the old
binding, (b) throwing an exception, or (c) safely wrapping the
result up with Maybe
lookupAssoc :: (Show1 (Sing :: k > *), JmEq1 (Sing :: k > *)) => Variable (a :: k) > Assocs ast > Maybe (ast a) Source #
Look up a variable and return the associated term.
N.B., this function is robust to all interpretations of varEq
.