Coercions

For convenience, Hakaru offers functions to convert between the four different numeric types in the language. These types are

• nat - Natural numbers
• int - Integers
• prob - Positive real numbers
• real - Real numbers

Amongst these types there are a collection of safe and unsafe coercions. A safe coercion is one which is always guaranteed to be valid. For example, converting a nat to an int is always safe. Converting an int to a nat is unsafe as the value can negative, and lead to runtime errors.

These are represented in the AST using the CoerceTo and UnsafeFrom constructors. Note that coercions are always defined in terms of the safe direction to go to.

CoerceTo_   :: !(Coercion a b) -> SCon '[ LC a ] b
UnsafeFrom_ :: !(Coercion a b) -> SCon '[ LC b ] a

Internally, coercions are specified using the Coercion datatype. This datatype states that each coercion is made up of a series of primitive coercions.

data Coercion :: Hakaru -> Hakaru -> * where
    CNil :: Coercion a a
    CCons :: !(PrimCoercion a b) -> !(Coercion b c) -> Coercion a c

These primitive coercions can either involve loosening a restriction on the sign of the value, or changing the numeric value to be over a continuous value. For example, to coerce from int to real, we would have a single Coercion with a PrimCoercion in it with the Continuous data constructor.

data PrimCoercion :: Hakaru -> Hakaru -> * where
    Signed     :: !(HRing a)       -> PrimCoercion (NonNegative a) a
    Continuous :: !(HContinuous a) -> PrimCoercion (HIntegral   a) a