hakaru-0.3.0: A probabilistic programming language

Language.Hakaru.Syntax.Variable

Description

An implementation of variables, for use with Language.Hakaru.Syntax.ABT.

Synopsis

# Our basic notion of variables.

data Variable a Source #

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 tie-the-knot in binder.

Constructors

 Variable FieldsvarHint :: !Text varID :: Nat varType :: !(Sing a)

Instances

 Eq1 k (Variable k) Source # Methodseq1 :: a i -> a i -> Bool Source # Show1 k (Sing k) => Show1 k (Variable k) Source # MethodsshowsPrec1 :: Int -> a i -> ShowS Source #show1 :: a i -> String Source # Eq (Variable k a) Source # Methods(==) :: Variable k a -> Variable k a -> Bool #(/=) :: Variable k a -> Variable k a -> Bool # Ord (Variable k a) Source # Methodscompare :: Variable k a -> Variable k a -> Ordering #(<) :: Variable k a -> Variable k a -> Bool #(<=) :: Variable k a -> Variable k a -> Bool #(>) :: Variable k a -> Variable k a -> Bool #(>=) :: Variable k a -> Variable k a -> Bool #max :: Variable k a -> Variable k a -> Variable k a #min :: Variable k a -> Variable k a -> Variable k a # Show (Sing k a) => Show (Variable k a) Source # MethodsshowsPrec :: Int -> Variable k a -> ShowS #show :: Variable k a -> String #showList :: [Variable k a] -> ShowS #

varEq :: (Show1 (Sing :: k -> *), JmEq1 (Sing :: k -> *)) => Variable (a :: k) -> Variable (b :: k) -> Maybe (TypeEq a b) Source #

Compare to variables at possibly-different 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 varTypes do not match the variables are not equal. Upside: we can statically guarantee that every variable is "well-typed" (by fiat). Downside: every type has its own variable namespace, which is very confusing. Also, the Ord SomeVariable instance will be really difficult to get right.
• We could require that whenever two varIDs match, their varTypes 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) an VarEqTypeError exception.
• We could assert that whenever two varIDs match, their varTypes 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.

Constructors

 VarEqTypeError :: (Show1 (Sing :: k -> *), JmEq1 (Sing :: k -> *)) => !(Variable (a :: k)) -> !(Variable (b :: k)) -> VarEqTypeError

Instances

 Source # MethodsshowList :: [VarEqTypeError] -> ShowS # Source # Methods

## 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 poly-kinded, 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!

Constructors

 SomeVariable !(Variable (a :: k))

Instances

 (JmEq1 k (Sing k), Show1 k (Sing k)) => Eq (SomeVariable k kproxy) Source # Methods(==) :: SomeVariable k kproxy -> SomeVariable k kproxy -> Bool #(/=) :: SomeVariable k kproxy -> SomeVariable k kproxy -> Bool # (JmEq1 k (Sing k), Show1 k (Sing k)) => Ord (SomeVariable k kproxy) Source # Methodscompare :: SomeVariable k kproxy -> SomeVariable k kproxy -> Ordering #(<) :: SomeVariable k kproxy -> SomeVariable k kproxy -> Bool #(<=) :: SomeVariable k kproxy -> SomeVariable k kproxy -> Bool #(>) :: SomeVariable k kproxy -> SomeVariable k kproxy -> Bool #(>=) :: SomeVariable k kproxy -> SomeVariable k kproxy -> Bool #max :: SomeVariable k kproxy -> SomeVariable k kproxy -> SomeVariable k kproxy #min :: SomeVariable k kproxy -> SomeVariable k kproxy -> SomeVariable k kproxy # Show1 k (Sing k) => Show (SomeVariable k kproxy) Source # MethodsshowsPrec :: Int -> SomeVariable k kproxy -> ShowS #show :: SomeVariable k kproxy -> String #showList :: [SomeVariable k kproxy] -> ShowS #

# Some helper types for "heaps", "environments", etc

## Typing environments; aka: sets of (typed) variables

newtype VarSet kproxy Source #

A set of (typed) variables.

Constructors

 VarSet FieldsunVarSet :: IntMap (SomeVariable kproxy)

Instances

 Show1 k (Sing k) => Show (VarSet k kproxy) Source # MethodsshowsPrec :: Int -> VarSet k kproxy -> ShowS #show :: VarSet k kproxy -> String #showList :: [VarSet k kproxy] -> ShowS # Monoid (VarSet k kproxy) Source # Methodsmempty :: VarSet k kproxy #mappend :: VarSet k kproxy -> VarSet k kproxy -> VarSet k kproxy #mconcat :: [VarSet k kproxy] -> VarSet k kproxy #

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 non-zero for non-empty sets.

## Substitutions; aka: maps from variables to their definitions

data Assoc ast Source #

A pair of variable and term, both of the same Hakaru type.

Constructors

 Assoc !(Variable a) !(ast a)

Instances

 (Show1 k (Sing k), Show1 k ast) => Show (Assoc k ast) Source # MethodsshowsPrec :: Int -> Assoc k ast -> ShowS #show :: Assoc k ast -> String #showList :: [Assoc k ast] -> ShowS #

newtype Assocs ast Source #

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.

Constructors

 Assocs FieldsunAssocs :: IntMap (Assoc ast)

Instances

 (Show1 k (Sing k), Show1 k ast) => Show (Assocs k ast) Source # MethodsshowsPrec :: Int -> Assocs k ast -> ShowS #show :: Assocs k ast -> String #showList :: [Assocs k ast] -> ShowS # Monoid (Assocs k abt) Source # Methodsmempty :: Assocs k abt #mappend :: Assocs k abt -> Assocs k abt -> Assocs k abt #mconcat :: [Assocs k abt] -> Assocs k abt #

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

insertAssocs :: Assocs ast -> Assocs ast -> Assocs ast Source #

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.

adjustAssoc :: Variable (a :: k) -> (Assoc ast -> Assoc ast) -> Assocs ast -> Assocs ast Source #

Adjust an association so existing variable refers to different value. Does nothing if variable not present.

mapAssocs :: (Assoc ast1 -> Assoc ast2) -> Assocs ast1 -> Assocs ast2 Source #