Copyright | Copyright (c) 2016 the Hakaru team |
---|---|
License | BSD3 |
Maintainer | wren@community.haskell.org |
Stability | experimental |
Portability | GHC-only |
Safe Haskell | None |
Language | Haskell2010 |
Our theory of coercions for Hakaru's numeric hierarchy.
Synopsis
- data PrimCoercion :: Hakaru -> Hakaru -> * where
- Signed :: !(HRing a) -> PrimCoercion (NonNegative a) a
- Continuous :: !(HContinuous a) -> PrimCoercion (HIntegral a) a
- class PrimCoerce (f :: Hakaru -> *) where
- data Coercion :: Hakaru -> Hakaru -> * where
- singletonCoercion :: PrimCoercion a b -> Coercion a b
- signed :: HRing_ a => Coercion (NonNegative a) a
- continuous :: HContinuous_ a => Coercion (HIntegral a) a
- class Coerce (f :: Hakaru -> *) where
- singCoerceDom :: Coercion a b -> Maybe (Sing a)
- singCoerceCod :: Coercion a b -> Maybe (Sing b)
- singCoerceDomCod :: Coercion a b -> Maybe (Sing a, Sing b)
- data CoercionMode a b
- findCoercion :: Sing a -> Sing b -> Maybe (Coercion a b)
- findEitherCoercion :: Sing a -> Sing b -> Maybe (CoercionMode a b)
- data Lub (a :: Hakaru) (b :: Hakaru) = Lub !(Sing c) !(Coercion a c) !(Coercion b c)
- findLub :: Sing a -> Sing b -> Maybe (Lub a b)
- data SomeRing (a :: Hakaru) = SomeRing !(HRing b) !(Coercion a b)
- findRing :: Sing a -> Maybe (SomeRing a)
- data SomeFractional (a :: Hakaru) = SomeFractional !(HFractional b) !(Coercion a b)
- findFractional :: Sing a -> Maybe (SomeFractional a)
- data ZigZag :: Hakaru -> Hakaru -> * where
- simplifyZZ :: ZigZag a b -> ZigZag a b
The primitive coercions
data PrimCoercion :: Hakaru -> Hakaru -> * where Source #
Primitive proofs of the inclusions in our numeric hierarchy.
Signed :: !(HRing a) -> PrimCoercion (NonNegative a) a | |
Continuous :: !(HContinuous a) -> PrimCoercion (HIntegral a) a |
Instances
JmEq2 PrimCoercion Source # | |
jmEq2 :: PrimCoercion i1 j1 -> PrimCoercion i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2) Source # | |
Eq2 PrimCoercion Source # | |
eq2 :: PrimCoercion i j -> PrimCoercion i j -> Bool Source # | |
JmEq1 (PrimCoercion a :: Hakaru -> *) Source # | |
jmEq1 :: PrimCoercion a i -> PrimCoercion a j -> Maybe (TypeEq i j) Source # | |
Eq1 (PrimCoercion a :: Hakaru -> *) Source # | |
eq1 :: PrimCoercion a i -> PrimCoercion a i -> Bool Source # | |
Eq (PrimCoercion a b) Source # | |
(==) :: PrimCoercion a b -> PrimCoercion a b -> Bool # (/=) :: PrimCoercion a b -> PrimCoercion a b -> Bool # | |
Show (PrimCoercion a b) Source # | |
showsPrec :: Int -> PrimCoercion a b -> ShowS # show :: PrimCoercion a b -> String # showList :: [PrimCoercion a b] -> ShowS # |
class PrimCoerce (f :: Hakaru -> *) 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)
primCoerceTo :: PrimCoercion a b -> f a -> f b Source #
primCoerceFrom :: PrimCoercion a b -> f b -> f a Source #
Instances
PrimCoerce Value Source # | |
primCoerceTo :: PrimCoercion a b -> Value a -> Value b Source # primCoerceFrom :: PrimCoercion a b -> Value b -> Value a Source # | |
PrimCoerce Literal Source # | |
primCoerceTo :: PrimCoercion a b -> Literal a -> Literal b Source # primCoerceFrom :: PrimCoercion a b -> Literal b -> Literal a Source # | |
PrimCoerce (Sing :: Hakaru -> *) Source # | |
primCoerceTo :: PrimCoercion a b -> Sing a -> Sing b Source # primCoerceFrom :: PrimCoercion a b -> Sing b -> Sing 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
).
singletonCoercion :: PrimCoercion a b -> Coercion a b Source #
A smart constructor for lifting PrimCoercion
into Coercion
continuous :: HContinuous_ a => Coercion (HIntegral a) a Source #
A smart constructor for Continuous
.
class Coerce (f :: Hakaru -> *) 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)
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 #
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 :: Hakaru) (b :: Hakaru) 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.
findLub :: Sing a -> Sing b -> Maybe (Lub a b) Source #
Given two types, find their least upper bound.
findRing :: Sing a -> Maybe (SomeRing a) Source #
Give a type, finds the smallest coercion to another with a HRing instance
data SomeFractional (a :: Hakaru) Source #
SomeFractional !(HFractional b) !(Coercion a b) |
findFractional :: Sing a -> Maybe (SomeFractional a) Source #
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.
simplifyZZ :: ZigZag a b -> ZigZag a b Source #