Language.Hakaru.Types.Coercion

Our theory of coercions for Hakaru's numeric hierarchy.

The primitive coercions

data PrimCoercion :: Hakaru -> Hakaru -> * where

Primitive proofs of the inclusions in our numeric hierarchy.

Constructors

Signed :: !(HRing a) -> PrimCoercion (NonNegative a) a

Continuous :: !(HContinuous a) -> PrimCoercion (HIntegral a) a

Instances

JmEq2 Hakaru Hakaru PrimCoercion

Methods

jmEq2 :: a i1 j1 -> a i2 j2 -> Maybe (TypeEq k1 i1 i2, TypeEq PrimCoercion j1 j2)

Eq2 Hakaru Hakaru PrimCoercion

Methods

eq2 :: a i j -> a i j -> Bool

JmEq1 Hakaru (PrimCoercion a)

Methods

jmEq1 :: a i -> a j -> Maybe (TypeEq (PrimCoercion a) i j)

Eq1 Hakaru (PrimCoercion a)

Methods

eq1 :: a i -> a i -> Bool

Eq (PrimCoercion a b)

Methods

(==) :: PrimCoercion a b -> PrimCoercion a b -> Bool

(/=) :: PrimCoercion a b -> PrimCoercion a b -> Bool

Show (PrimCoercion a b)

Methods

showsPrec :: Int -> PrimCoercion a b -> ShowS

show :: PrimCoercion a b -> String

showList :: [PrimCoercion a b] -> ShowS

class PrimCoerce f where

This class defines a mapping from PrimCoercion to the (->) category. (Technically these mappings aren't functors, since PrimCoercion doesn't form a category.) It's mostly used for defining the analogous Coerce instance; that is, given a PrimCoerce F instance, we have the following canonical Coerce F instance:

instance Coerce F where
    coerceTo   CNil         s = s
    coerceTo   (CCons c cs) s = coerceTo cs (primCoerceTo c s)

    coerceFrom CNil         s = s
    coerceFrom (CCons c cs) s = primCoerceFrom c (coerceFrom cs s)

Minimal complete definition

primCoerceTo, primCoerceFrom

Methods

primCoerceTo :: PrimCoercion a b -> f a -> f b

primCoerceFrom :: PrimCoercion a b -> f b -> f a

Instances

PrimCoerce Literal

Methods

primCoerceTo :: PrimCoercion a b -> Literal a -> Literal b

primCoerceFrom :: PrimCoercion a b -> Literal b -> Literal a

PrimCoerce Value

Methods

primCoerceTo :: PrimCoercion a b -> Value a -> Value b

primCoerceFrom :: PrimCoercion a b -> Value b -> Value a

PrimCoerce (Sing Hakaru)

Methods

primCoerceTo :: PrimCoercion a b -> Sing Hakaru a -> Sing Hakaru b

primCoerceFrom :: PrimCoercion a b -> Sing Hakaru b -> Sing Hakaru a

The category of general coercions

data Coercion :: Hakaru -> Hakaru -> * where

General proofs of the inclusions in our numeric hierarchy. Notably, being a partial order, Coercion forms a category. In addition to the Category instance, we also have the class Coerce for functors from Coercion to the category of Haskell functions, and you can get the co/domain objects (via singCoerceDom, singCoerceCod, or singCoerceDomCod).

Constructors

CNil :: Coercion a a

CCons :: !(PrimCoercion a b) -> !(Coercion b c) -> Coercion a c

Instances

Category Hakaru Coercion

Methods

id :: cat a a

(.) :: cat b c -> cat a b -> cat a c

Eq2 Hakaru Hakaru Coercion

Methods

eq2 :: a i j -> a i j -> Bool

Eq1 Hakaru (Coercion a)

Methods

eq1 :: a i -> a i -> Bool

Eq (Coercion a b)

Methods

(==) :: Coercion a b -> Coercion a b -> Bool

(/=) :: Coercion a b -> Coercion a b -> Bool

Show (Coercion a b)

Methods

showsPrec :: Int -> Coercion a b -> ShowS

show :: Coercion a b -> String

showList :: [Coercion a b] -> ShowS

singletonCoercion :: PrimCoercion a b -> Coercion a b

A smart constructor for lifting PrimCoercion into Coercion

signed :: HRing_ a => Coercion (NonNegative a) a

A smart constructor for Signed.

continuous :: HContinuous_ a => Coercion (HIntegral a) a

A smart constructor for Continuous.

class Coerce f where

This class defines functors from the Coercion category to the (->) category. It's mostly used for defining smart constructors that implement the coercion in f. We don't require a PrimCoerce constraint (because we never need it), but given a Coerce F instance, we have the following canonical PrimCoerce F instance:

instance PrimCoerce F where
    primCoerceTo   c = coerceTo   (singletonCoercion c)
    primCoerceFrom c = coerceFrom (singletonCoercion c)

Minimal complete definition

coerceTo, coerceFrom

Methods

coerceTo :: Coercion a b -> f a -> f b

coerceFrom :: Coercion a b -> f b -> f a

Instances

Coerce Literal

Methods

coerceTo :: Coercion a b -> Literal a -> Literal b

coerceFrom :: Coercion a b -> Literal b -> Literal a

Coerce Value

Methods

coerceTo :: Coercion a b -> Value a -> Value b

coerceFrom :: Coercion a b -> Value b -> Value a

Coerce (Sing Hakaru)

Methods

coerceTo :: Coercion a b -> Sing Hakaru a -> Sing Hakaru b

coerceFrom :: Coercion a b -> Sing Hakaru b -> Sing Hakaru a

ABT Hakaru Term abt => Coerce (LC_ abt)

Methods

coerceTo :: Coercion a b -> LC_ abt a -> LC_ abt b

coerceFrom :: Coercion a b -> LC_ abt b -> LC_ abt a

ABT Hakaru Term abt => Coerce (Term abt)

Methods

coerceTo :: Coercion a b -> Term abt a -> Term abt b

coerceFrom :: Coercion a b -> Term abt b -> Term abt a

ABT Hakaru Term abt => Coerce (Whnf abt)

Methods

coerceTo :: Coercion a b -> Whnf abt a -> Whnf abt b

coerceFrom :: Coercion a b -> Whnf abt b -> Whnf abt a

singCoerceDom :: Coercion a b -> Maybe (Sing a)

Return a singleton for the domain type, or Nothing if it's the CNil coercion.

singCoerceCod :: Coercion a b -> Maybe (Sing b)

Return a singleton for the codomain type, or Nothing if it's the CNil coercion.

singCoerceDomCod :: Coercion a b -> Maybe (Sing a, Sing b)

Return singletons for the domain and codomain types, or Nothing if it's the CNil coercion. If you need both types, this is a bit more efficient than calling singCoerceDom and singCoerceCod separately.

The induced coercion hierarchy

data CoercionMode a b

Constructors

Safe (Coercion a b)

Unsafe (Coercion b a)

Mixed (Sing c, Coercion c a, Coercion c b)

findCoercion :: Sing a -> Sing b -> Maybe (Coercion a b)

Given two types, find a coercion from the first to the second, or return Nothing if there is no such coercion.

findEitherCoercion :: Sing a -> Sing b -> Maybe (CoercionMode a b)

Given two types, find either a coercion from the first to the second or a coercion from the second to the first, or returns Nothing if there is neither such coercion.

If the two types are equal, then we preferentially return the Coercion a b. The ordering of the Either is so that we consider the Coercion a b direction "success" in the Either monad (which also expresses our bias when the types are equal).

data Lub a b

An upper bound of two types, with the coercions witnessing its upperbound-ness. The type itself ensures that we have some upper bound; but in practice we assume it is in fact the least upper bound.

Constructors

Lub !(Sing c) !(Coercion a c) !(Coercion b c)

findLub :: Sing a -> Sing b -> Maybe (Lub a b)

Given two types, find their least upper bound.

data SomeRing a

Constructors

SomeRing !(HRing b) !(Coercion a b)

findRing :: Sing a -> Maybe (SomeRing a)

Give a type, finds the smallest coercion to another with a HRing instance

data SomeFractional a

Constructors

SomeFractional !(HFractional b) !(Coercion a b)

findFractional :: Sing a -> Maybe (SomeFractional a)

Give a type, finds the smallest coercion to another with a HFractional instance

Experimental optimization functions

data ZigZag :: Hakaru -> Hakaru -> * where

An arbitrary composition of safe and unsafe coercions.

Constructors

ZRefl :: ZigZag a a

Zig :: !(Coercion a b) -> !(ZigZag b c) -> ZigZag a c

Zag :: !(Coercion b a) -> !(ZigZag b c) -> ZigZag a c

Instances

Show (ZigZag a b)

Methods

showsPrec :: Int -> ZigZag a b -> ShowS

show :: ZigZag a b -> String

showList :: [ZigZag a b] -> ShowS

simplifyZZ :: ZigZag a b -> ZigZag a b