Copyright	Copyright (c) 2016 the Hakaru team
License	BSD3
Maintainer	wren@community.haskell.org
Stability	experimental
Portability	GHC-only
Safe Haskell	None
Language	Haskell2010

Language.Hakaru.Types.Coercion

Contents

The primitive coercions
The category of general coercions
The induced coercion hierarchy
Experimental optimization functions

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

JmEq2 Hakaru Hakaru PrimCoercion Source #
Methods jmEq2 :: a i1 j1 -> a i2 j2 -> Maybe (TypeEq k1 i1 i2, TypeEq PrimCoercion j1 j2) Source #
Eq2 Hakaru Hakaru PrimCoercion Source #
Methods eq2 :: a i j -> a i j -> Bool Source #
JmEq1 Hakaru (PrimCoercion a) Source #
Methods jmEq1 :: a i -> a j -> Maybe (TypeEq (PrimCoercion a) i j) Source #
Eq1 Hakaru (PrimCoercion a) Source #
Methods eq1 :: 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 #
Methods showsPrec :: 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

primCoerceTo, primCoerceFrom

Methods

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

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

Instances

PrimCoerce Literal Source #
Methods primCoerceTo :: PrimCoercion a b -> Literal a -> Literal b Source # primCoerceFrom :: PrimCoercion a b -> Literal b -> Literal a Source #
PrimCoerce Value Source #
Methods primCoerceTo :: PrimCoercion a b -> Value a -> Value b Source # primCoerceFrom :: PrimCoercion a b -> Value b -> Value a Source #
PrimCoerce (Sing Hakaru) Source #
Methods primCoerceTo :: PrimCoercion a b -> Sing Hakaru a -> Sing Hakaru b Source # primCoerceFrom :: PrimCoercion a b -> Sing Hakaru b -> Sing Hakaru a 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

Category Hakaru Coercion Source #
Methods id :: cat a a # (.) :: cat b c -> cat a b -> cat a c #
Eq2 Hakaru Hakaru Coercion Source #
Methods eq2 :: a i j -> a i j -> Bool Source #
Eq1 Hakaru (Coercion a) Source #
Methods eq1 :: 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 #
Methods showsPrec :: 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.

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

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

coerceTo, coerceFrom

Methods

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

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

Instances

Coerce Literal Source #
Methods coerceTo :: Coercion a b -> Literal a -> Literal b Source # coerceFrom :: Coercion a b -> Literal b -> Literal a Source #
Coerce Value Source #
Methods coerceTo :: Coercion a b -> Value a -> Value b Source # coerceFrom :: Coercion a b -> Value b -> Value a Source #
Coerce (Sing Hakaru) Source #
Methods coerceTo :: 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 #
Methods coerceTo :: 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 #
Methods coerceTo :: 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 #
Methods coerceTo :: 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

data SomeFractional a Source #

Constructors

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