| 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.HClasses
Description
A collection of type classes for encoding Hakaru's numeric hierarchy.
Synopsis
- data HEq :: Hakaru -> * where
- class HEq_ (a :: Hakaru) where
- sing_HEq :: HEq a -> Sing a
- hEq_Sing :: Sing a -> Maybe (HEq a)
- data HOrd :: Hakaru -> * where
- hEq_HOrd :: HOrd a -> HEq a
- class HEq_ a => HOrd_ (a :: Hakaru) where
- sing_HOrd :: HOrd a -> Sing a
- hOrd_Sing :: Sing a -> Maybe (HOrd a)
- data HIntegrable :: Hakaru -> * where
- sing_HIntegrable :: HIntegrable a -> Sing a
- hIntegrable_Sing :: Sing a -> Maybe (HIntegrable a)
- data HSemiring :: Hakaru -> * where
- class HSemiring_ (a :: Hakaru) where
- sing_HSemiring :: HSemiring a -> Sing a
- hSemiring_Sing :: Sing a -> Maybe (HSemiring a)
- data HRing :: Hakaru -> * where
- hSemiring_HRing :: HRing a -> HSemiring a
- hSemiring_NonNegativeHRing :: HRing a -> HSemiring (NonNegative a)
- class (HSemiring_ (NonNegative a), HSemiring_ a) => HRing_ (a :: Hakaru) where
- type NonNegative (a :: Hakaru) :: Hakaru
- hRing :: HRing a
- sing_HRing :: HRing a -> Sing a
- hRing_Sing :: Sing a -> Maybe (HRing a)
- sing_NonNegative :: HRing a -> Sing (NonNegative a)
- data HFractional :: Hakaru -> * where
- hSemiring_HFractional :: HFractional a -> HSemiring a
- class HSemiring_ a => HFractional_ (a :: Hakaru) where
- hFractional :: HFractional a
- sing_HFractional :: HFractional a -> Sing a
- hFractional_Sing :: Sing a -> Maybe (HFractional a)
- data HRadical :: Hakaru -> * where
- hSemiring_HRadical :: HRadical a -> HSemiring a
- class HSemiring_ a => HRadical_ (a :: Hakaru) where
- sing_HRadical :: HRadical a -> Sing a
- hRadical_Sing :: Sing a -> Maybe (HRadical a)
- data HDiscrete :: Hakaru -> * where
- class HSemiring_ a => HDiscrete_ (a :: Hakaru) where
- sing_HDiscrete :: HDiscrete a -> Sing a
- hDiscrete_Sing :: Sing a -> Maybe (HDiscrete a)
- data HContinuous :: Hakaru -> * where
- hFractional_HContinuous :: HContinuous a -> HFractional a
- hSemiring_HIntegralContinuous :: HContinuous a -> HSemiring (HIntegral a)
- class (HSemiring_ (HIntegral a), HFractional_ a) => HContinuous_ (a :: Hakaru) where
- type HIntegral (a :: Hakaru) :: Hakaru
- hContinuous :: HContinuous a
- sing_HContinuous :: HContinuous a -> Sing a
- hContinuous_Sing :: Sing a -> Maybe (HContinuous a)
- sing_HIntegral :: HContinuous a -> Sing (HIntegral a)
Equality
data HEq :: Hakaru -> * where Source #
Concrete dictionaries for Hakaru types with decidable equality.
Constructors
| HEq_Nat :: HEq 'HNat | |
| HEq_Int :: HEq 'HInt | |
| HEq_Prob :: HEq 'HProb | |
| HEq_Real :: HEq 'HReal | |
| HEq_Array :: !(HEq a) -> HEq ('HArray a) | |
| HEq_Bool :: HEq HBool | |
| HEq_Unit :: HEq HUnit | |
| HEq_Pair :: !(HEq a) -> !(HEq b) -> HEq (HPair a b) | |
| HEq_Either :: !(HEq a) -> !(HEq b) -> HEq (HEither a b) |
Instances
class HEq_ (a :: Hakaru) where Source #
Haskell type class for automatic HEq inference.
Ordering
data HOrd :: Hakaru -> * where Source #
Concrete dictionaries for Hakaru types with decidable total ordering.
Constructors
| HOrd_Nat :: HOrd 'HNat | |
| HOrd_Int :: HOrd 'HInt | |
| HOrd_Prob :: HOrd 'HProb | |
| HOrd_Real :: HOrd 'HReal | |
| HOrd_Array :: !(HOrd a) -> HOrd ('HArray a) | |
| HOrd_Bool :: HOrd HBool | |
| HOrd_Unit :: HOrd HUnit | |
| HOrd_Pair :: !(HOrd a) -> !(HOrd b) -> HOrd (HPair a b) | |
| HOrd_Either :: !(HOrd a) -> !(HOrd b) -> HOrd (HEither a b) |
class HEq_ a => HOrd_ (a :: Hakaru) where Source #
Haskell type class for automatic HOrd inference.
HIntegrable
data HIntegrable :: Hakaru -> * where Source #
Concrete dictionaries for types where Infinity can have
Constructors
| HIntegrable_Nat :: HIntegrable 'HNat | |
| HIntegrable_Prob :: HIntegrable 'HProb |
Instances
| JmEq1 HIntegrable Source # | |
Defined in Language.Hakaru.Types.HClasses Methods jmEq1 :: forall (i :: k) (j :: k). HIntegrable i -> HIntegrable j -> Maybe (TypeEq i j) Source # | |
| Eq1 HIntegrable Source # | |
Defined in Language.Hakaru.Types.HClasses Methods eq1 :: forall (i :: k). HIntegrable i -> HIntegrable i -> Bool Source # | |
| Eq (HIntegrable a) Source # | |
Defined in Language.Hakaru.Types.HClasses Methods (==) :: HIntegrable a -> HIntegrable a -> Bool # (/=) :: HIntegrable a -> HIntegrable a -> Bool # | |
| Show (HIntegrable a) Source # | |
Defined in Language.Hakaru.Types.HClasses Methods showsPrec :: Int -> HIntegrable a -> ShowS # show :: HIntegrable a -> String # showList :: [HIntegrable a] -> ShowS # | |
sing_HIntegrable :: HIntegrable a -> Sing a Source #
hIntegrable_Sing :: Sing a -> Maybe (HIntegrable a) Source #
Semirings
data HSemiring :: Hakaru -> * where Source #
Concrete dictionaries for Hakaru types which are semirings. N.B., even though these particular semirings are commutative, we don't necessarily assume that.
Constructors
| HSemiring_Nat :: HSemiring 'HNat | |
| HSemiring_Int :: HSemiring 'HInt | |
| HSemiring_Prob :: HSemiring 'HProb | |
| HSemiring_Real :: HSemiring 'HReal |
class HSemiring_ (a :: Hakaru) where Source #
Haskell type class for automatic HSemiring inference.
Instances
sing_HSemiring :: HSemiring a -> Sing a Source #
Rings
data HRing :: Hakaru -> * where Source #
Concrete dictionaries for Hakaru types which are rings. N.B., even though these particular rings are commutative, we don't necessarily assume that.
hSemiring_NonNegativeHRing :: HRing a -> HSemiring (NonNegative a) Source #
class (HSemiring_ (NonNegative a), HSemiring_ a) => HRing_ (a :: Hakaru) where Source #
Haskell type class for automatic HRing inference.
Every HRing has an associated type for the semiring of its
non-negative elements. This type family captures two notions.
First, if we take the semiring and close it under negation/subtraction
then we will generate this ring. Second, when we take the absolute
value of something in the ring we will get back something in the
non-negative semiring. For HInt and HReal these two notions
coincide; however for Complex and Vector types, the notions
diverge.
TODO: Can we somehow specify that the HSemiring (NonNegative
a) semantics coincides with the HSemiring a semantics? Or
should we just assume that?
Associated Types
type NonNegative (a :: Hakaru) :: Hakaru Source #
sing_HRing :: HRing a -> Sing a Source #
sing_NonNegative :: HRing a -> Sing (NonNegative a) Source #
Fractional types
data HFractional :: Hakaru -> * where Source #
Concrete dictionaries for Hakaru types which are division-semirings; i.e., division-rings without negation. This is called a "semifield" in ring theory, but should not be confused with the "semifields" of geometry.
Constructors
| HFractional_Prob :: HFractional 'HProb | |
| HFractional_Real :: HFractional 'HReal |
Instances
| JmEq1 HFractional Source # | |
Defined in Language.Hakaru.Types.HClasses Methods jmEq1 :: forall (i :: k) (j :: k). HFractional i -> HFractional j -> Maybe (TypeEq i j) Source # | |
| Eq1 HFractional Source # | |
Defined in Language.Hakaru.Types.HClasses Methods eq1 :: forall (i :: k). HFractional i -> HFractional i -> Bool Source # | |
| Eq (HFractional a) Source # | |
Defined in Language.Hakaru.Types.HClasses Methods (==) :: HFractional a -> HFractional a -> Bool # (/=) :: HFractional a -> HFractional a -> Bool # | |
| Show (HFractional a) Source # | |
Defined in Language.Hakaru.Types.HClasses Methods showsPrec :: Int -> HFractional a -> ShowS # show :: HFractional a -> String # showList :: [HFractional a] -> ShowS # | |
hSemiring_HFractional :: HFractional a -> HSemiring a Source #
Every HFractional is a HSemiring.
class HSemiring_ a => HFractional_ (a :: Hakaru) where Source #
Haskell type class for automatic HFractional inference.
Methods
hFractional :: HFractional a Source #
Instances
| HFractional_ 'HProb Source # | |
Defined in Language.Hakaru.Types.HClasses Methods | |
| HFractional_ 'HReal Source # | |
Defined in Language.Hakaru.Types.HClasses Methods | |
sing_HFractional :: HFractional a -> Sing a Source #
hFractional_Sing :: Sing a -> Maybe (HFractional a) Source #
Radical types
data HRadical :: Hakaru -> * where Source #
Concrete dictionaries for semirings which are closed under all
HNat-roots. This means it's closed under all positive rational
powers as well. (If the type happens to be HFractional, then
it's closed under all rational powers.)
N.B., HReal is not HRadical because we do not have real-valued
roots for negative reals.
N.B., we assume not only that the type is surd-complete, but
also that it's still complete under the semiring operations.
Thus we have values like sqrt 2 + sqrt 3 which cannot be
expressed as a single root. Thus, in order to solve for zeros/roots,
we'll need solutions to more general polynomials than just the
x^n - a polynomials. However, the Galois groups of these are
all solvable, so this shouldn't be too bad.
Constructors
| HRadical_Prob :: HRadical 'HProb |
class HSemiring_ a => HRadical_ (a :: Hakaru) where Source #
Haskell type class for automatic HRadical inference.
sing_HRadical :: HRadical a -> Sing a Source #
Discrete types
data HDiscrete :: Hakaru -> * where Source #
Concrete dictionaries for Hakaru types which are "discrete".
Constructors
| HDiscrete_Nat :: HDiscrete 'HNat | |
| HDiscrete_Int :: HDiscrete 'HInt |
class HSemiring_ a => HDiscrete_ (a :: Hakaru) where Source #
Haskell type class for automatic HDiscrete inference.
Instances
sing_HDiscrete :: HDiscrete a -> Sing a Source #
Continuous types
data HContinuous :: Hakaru -> * where Source #
Concrete dictionaries for Hakaru types which are "continuous".
This is an ad-hoc class for (a) lifting HNat/HInt into
HProb/HReal, and (b) handling the polymorphism of monotonic
functions like etf.
Constructors
| HContinuous_Prob :: HContinuous 'HProb | |
| HContinuous_Real :: HContinuous 'HReal |
Instances
| JmEq1 HContinuous Source # | |
Defined in Language.Hakaru.Types.HClasses Methods jmEq1 :: forall (i :: k) (j :: k). HContinuous i -> HContinuous j -> Maybe (TypeEq i j) Source # | |
| Eq1 HContinuous Source # | |
Defined in Language.Hakaru.Types.HClasses Methods eq1 :: forall (i :: k). HContinuous i -> HContinuous i -> Bool Source # | |
| Eq (HContinuous a) Source # | |
Defined in Language.Hakaru.Types.HClasses Methods (==) :: HContinuous a -> HContinuous a -> Bool # (/=) :: HContinuous a -> HContinuous a -> Bool # | |
| Show (HContinuous a) Source # | |
Defined in Language.Hakaru.Types.HClasses Methods showsPrec :: Int -> HContinuous a -> ShowS # show :: HContinuous a -> String # showList :: [HContinuous a] -> ShowS # | |
hFractional_HContinuous :: HContinuous a -> HFractional a Source #
Every HContinuous is a HFractional.
hSemiring_HIntegralContinuous :: HContinuous a -> HSemiring (HIntegral a) Source #
The integral type of every HContinuous is a HSemiring.
class (HSemiring_ (HIntegral a), HFractional_ a) => HContinuous_ (a :: Hakaru) where Source #
Haskell type class for automatic HContinuous inference.
Every HContinuous has an associated type for the semiring of
its integral elements.
TODO: Can we somehow specify that the HSemiring (HIntegral a)
semantics coincides with the HSemiring a semantics? Or should
we just assume that?
Methods
hContinuous :: HContinuous a Source #
Instances
| HContinuous_ 'HProb Source # | |
Defined in Language.Hakaru.Types.HClasses Methods | |
| HContinuous_ 'HReal Source # | |
Defined in Language.Hakaru.Types.HClasses Methods | |
sing_HContinuous :: HContinuous a -> Sing a Source #
hContinuous_Sing :: Sing a -> Maybe (HContinuous a) Source #
sing_HIntegral :: HContinuous a -> Sing (HIntegral a) Source #