hakaru-0.3.0: A probabilistic programming language

Language.Hakaru.Types.Coercion

Description

Our theory of coercions for Hakaru's numeric hierarchy.

Synopsis

# The primitive coercions

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

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

 Source # MethodsjmEq2 :: a i1 j1 -> a i2 j2 -> Maybe (TypeEq k1 i1 i2, TypeEq PrimCoercion j1 j2) Source # Source # Methodseq2 :: a i j -> a i j -> Bool Source # Source # MethodsjmEq1 :: a i -> a j -> Maybe (TypeEq (PrimCoercion a) i j) Source # Source # Methodseq1 :: a i -> a i -> Bool Source # Eq (PrimCoercion a b) Source # Methods(==) :: PrimCoercion a b -> PrimCoercion a b -> Bool #(/=) :: PrimCoercion a b -> PrimCoercion a b -> Bool # Show (PrimCoercion a b) Source # MethodsshowsPrec :: Int -> PrimCoercion a b -> ShowS #show :: PrimCoercion a b -> String #showList :: [PrimCoercion a b] -> ShowS #

class PrimCoerce f where Source #

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

Methods

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

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

Instances

 Source # MethodsprimCoerceTo :: PrimCoercion a b -> Literal a -> Literal b Source #primCoerceFrom :: PrimCoercion a b -> Literal b -> Literal a Source # Source # MethodsprimCoerceTo :: PrimCoercion a b -> Value a -> Value b Source #primCoerceFrom :: PrimCoercion a b -> Value b -> Value a Source # Source # MethodsprimCoerceTo :: PrimCoercion a b -> Sing Hakaru a -> Sing Hakaru b Source #

# The category of general coercions

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

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

 Source # Methodsid :: cat a a #(.) :: cat b c -> cat a b -> cat a c # Source # Methodseq2 :: a i j -> a i j -> Bool Source # Source # Methodseq1 :: a i -> a i -> Bool Source # Eq (Coercion a b) Source # Methods(==) :: Coercion a b -> Coercion a b -> Bool #(/=) :: Coercion a b -> Coercion a b -> Bool # Show (Coercion a b) Source # MethodsshowsPrec :: Int -> Coercion a b -> ShowS #show :: Coercion a b -> String #showList :: [Coercion a b] -> ShowS #

singletonCoercion :: PrimCoercion a b -> Coercion a b Source #

A smart constructor for lifting PrimCoercion into Coercion

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

A smart constructor for Signed.

A smart constructor for Continuous.

class Coerce f where Source #

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

Methods

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

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

Instances

 Source # MethodscoerceTo :: Coercion a b -> Literal a -> Literal b Source #coerceFrom :: Coercion a b -> Literal b -> Literal a Source # Source # MethodscoerceTo :: Coercion a b -> Value a -> Value b Source #coerceFrom :: Coercion a b -> Value b -> Value a Source # Source # MethodscoerceTo :: Coercion a b -> Sing Hakaru a -> Sing Hakaru b Source #coerceFrom :: Coercion a b -> Sing Hakaru b -> Sing Hakaru a Source # ABT Hakaru Term abt => Coerce (LC_ abt) Source # MethodscoerceTo :: Coercion a b -> LC_ abt a -> LC_ abt b Source #coerceFrom :: Coercion a b -> LC_ abt b -> LC_ abt a Source # ABT Hakaru Term abt => Coerce (Term abt) Source # MethodscoerceTo :: Coercion a b -> Term abt a -> Term abt b Source #coerceFrom :: Coercion a b -> Term abt b -> Term abt a Source # ABT Hakaru Term abt => Coerce (Whnf abt) Source # MethodscoerceTo :: Coercion a b -> Whnf abt a -> Whnf abt b Source #coerceFrom :: Coercion a b -> Whnf abt b -> Whnf abt a Source #

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

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

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

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

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

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 Source #

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) Source #

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) Source #

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 Source #

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) Source #

Given two types, find their least upper bound.

data SomeRing a Source #

Constructors

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

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

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

Constructors

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

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

# Experimental optimization functions

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

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) Source # MethodsshowsPrec :: Int -> ZigZag a b -> ShowS #show :: ZigZag a b -> String #showList :: [ZigZag a b] -> ShowS #