Language.Hakaru.Types.HClasses

A collection of type classes for encoding Hakaru's numeric hierarchy.

Equality

data HEq :: Hakaru -> * where

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

Eq (HEq a)

Methods

(==) :: HEq a -> HEq a -> Bool

(/=) :: HEq a -> HEq a -> Bool

Show (HEq a)

Methods

showsPrec :: Int -> HEq a -> ShowS

show :: HEq a -> String

showList :: [HEq a] -> ShowS

class HEq_ a where

Haskell type class for automatic HEq inference.

Minimal complete definition

hEq

Methods

hEq :: HEq a

Instances

HEq_ HUnit

Methods

hEq :: HEq HUnit

HEq_ HBool

Methods

hEq :: HEq HBool

HEq_ HNat

Methods

hEq :: HEq HNat

HEq_ HInt

Methods

hEq :: HEq HInt

HEq_ HProb

Methods

hEq :: HEq HProb

HEq_ HReal

Methods

hEq :: HEq HReal

HEq_ a => HEq_ (HArray a)

Methods

hEq :: HEq (HArray a)

(HEq_ a, HEq_ b) => HEq_ (HEither a b)

Methods

hEq :: HEq (HEither a b)

(HEq_ a, HEq_ b) => HEq_ (HPair a b)

Methods

hEq :: HEq (HPair a b)

sing_HEq :: HEq a -> Sing a

hEq_Sing :: Sing a -> Maybe (HEq a)

Ordering

data HOrd :: Hakaru -> * where

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)

Instances

Eq (HOrd a)

Methods

(==) :: HOrd a -> HOrd a -> Bool

(/=) :: HOrd a -> HOrd a -> Bool

Show (HOrd a)

Methods

showsPrec :: Int -> HOrd a -> ShowS

show :: HOrd a -> String

showList :: [HOrd a] -> ShowS

hEq_HOrd :: HOrd a -> HEq a

Every HOrd type is HEq.

class HEq_ a => HOrd_ a where

Haskell type class for automatic HOrd inference.

Minimal complete definition

hOrd

Methods

hOrd :: HOrd a

Instances

HOrd_ HUnit

Methods

hOrd :: HOrd HUnit

HOrd_ HBool

Methods

hOrd :: HOrd HBool

HOrd_ HNat

Methods

hOrd :: HOrd HNat

HOrd_ HInt

Methods

hOrd :: HOrd HInt

HOrd_ HProb

Methods

hOrd :: HOrd HProb

HOrd_ HReal

Methods

hOrd :: HOrd HReal

HOrd_ a => HOrd_ (HArray a)

Methods

hOrd :: HOrd (HArray a)

(HOrd_ a, HOrd_ b) => HOrd_ (HEither a b)

Methods

hOrd :: HOrd (HEither a b)

(HOrd_ a, HOrd_ b) => HOrd_ (HPair a b)

Methods

hOrd :: HOrd (HPair a b)

sing_HOrd :: HOrd a -> Sing a

hOrd_Sing :: Sing a -> Maybe (HOrd a)

HIntegrable

data HIntegrable :: Hakaru -> * where

Concrete dictionaries for types where Infinity can have

Constructors

HIntegrable_Nat :: HIntegrable HNat

HIntegrable_Prob :: HIntegrable HProb

Instances

JmEq1 Hakaru HIntegrable

Methods

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

Eq1 Hakaru HIntegrable

Methods

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

Eq (HIntegrable a)

Methods

(==) :: HIntegrable a -> HIntegrable a -> Bool

(/=) :: HIntegrable a -> HIntegrable a -> Bool

Show (HIntegrable a)

Methods

showsPrec :: Int -> HIntegrable a -> ShowS

show :: HIntegrable a -> String

showList :: [HIntegrable a] -> ShowS

sing_HIntegrable :: HIntegrable a -> Sing a

hIntegrable_Sing :: Sing a -> Maybe (HIntegrable a)

Semirings

data HSemiring :: Hakaru -> * where

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

Instances

JmEq1 Hakaru HSemiring

Methods

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

Eq1 Hakaru HSemiring

Methods

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

Eq (HSemiring a)

Methods

(==) :: HSemiring a -> HSemiring a -> Bool

(/=) :: HSemiring a -> HSemiring a -> Bool

Show (HSemiring a)

Methods

showsPrec :: Int -> HSemiring a -> ShowS

show :: HSemiring a -> String

showList :: [HSemiring a] -> ShowS

class HSemiring_ a where

Haskell type class for automatic HSemiring inference.

Minimal complete definition

hSemiring

Methods

hSemiring :: HSemiring a

Instances

HSemiring_ HNat

Methods

hSemiring :: HSemiring HNat

HSemiring_ HInt

Methods

hSemiring :: HSemiring HInt

HSemiring_ HProb

Methods

hSemiring :: HSemiring HProb

HSemiring_ HReal

Methods

hSemiring :: HSemiring HReal

sing_HSemiring :: HSemiring a -> Sing a

hSemiring_Sing :: Sing a -> Maybe (HSemiring a)

Rings

data HRing :: Hakaru -> * where

Concrete dictionaries for Hakaru types which are rings. N.B., even though these particular rings are commutative, we don't necessarily assume that.

Constructors

HRing_Int :: HRing HInt

HRing_Real :: HRing HReal

Instances

JmEq1 Hakaru HRing

Methods

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

Eq1 Hakaru HRing

Methods

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

Eq (HRing a)

Methods

(==) :: HRing a -> HRing a -> Bool

(/=) :: HRing a -> HRing a -> Bool

Show (HRing a)

Methods

showsPrec :: Int -> HRing a -> ShowS

show :: HRing a -> String

showList :: [HRing a] -> ShowS

hSemiring_HRing :: HRing a -> HSemiring a

Every HRing is a HSemiring.

hSemiring_NonNegativeHRing :: HRing a -> HSemiring (NonNegative a)

The non-negative type of every HRing is a HSemiring.

class (HSemiring_ (NonNegative a), HSemiring_ a) => HRing_ a where

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?

Minimal complete definition

hRing

Associated Types

type NonNegative (a :: Hakaru) :: Hakaru

Methods

hRing :: HRing a

Instances

HRing_ HInt

Associated Types

type NonNegative (HInt :: Hakaru) :: Hakaru

Methods

hRing :: HRing HInt

HRing_ HReal

Associated Types

type NonNegative (HReal :: Hakaru) :: Hakaru

Methods

hRing :: HRing HReal

sing_HRing :: HRing a -> Sing a

hRing_Sing :: Sing a -> Maybe (HRing a)

sing_NonNegative :: HRing a -> Sing (NonNegative a)

Fractional types

data HFractional :: Hakaru -> * where

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 Hakaru HFractional

Methods

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

Eq1 Hakaru HFractional

Methods

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

Eq (HFractional a)

Methods

(==) :: HFractional a -> HFractional a -> Bool

(/=) :: HFractional a -> HFractional a -> Bool

Show (HFractional a)

Methods

showsPrec :: Int -> HFractional a -> ShowS

show :: HFractional a -> String

showList :: [HFractional a] -> ShowS

hSemiring_HFractional :: HFractional a -> HSemiring a

Every HFractional is a HSemiring.

class HSemiring_ a => HFractional_ a where

Haskell type class for automatic HFractional inference.

Minimal complete definition

hFractional

Methods

hFractional :: HFractional a

Instances

HFractional_ HProb

Methods

hFractional :: HFractional HProb

HFractional_ HReal

Methods

hFractional :: HFractional HReal

sing_HFractional :: HFractional a -> Sing a

hFractional_Sing :: Sing a -> Maybe (HFractional a)

Radical types

data HRadical :: Hakaru -> * where

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

Instances

JmEq1 Hakaru HRadical

Methods

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

Eq1 Hakaru HRadical

Methods

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

Eq (HRadical a)

Methods

(==) :: HRadical a -> HRadical a -> Bool

(/=) :: HRadical a -> HRadical a -> Bool

Show (HRadical a)

Methods

showsPrec :: Int -> HRadical a -> ShowS

show :: HRadical a -> String

showList :: [HRadical a] -> ShowS

hSemiring_HRadical :: HRadical a -> HSemiring a

Every HRadical is a HSemiring.

class HSemiring_ a => HRadical_ a where

Haskell type class for automatic HRadical inference.

Minimal complete definition

hRadical

Methods

hRadical :: HRadical a

Instances

HRadical_ HProb

Methods

hRadical :: HRadical HProb

sing_HRadical :: HRadical a -> Sing a

hRadical_Sing :: Sing a -> Maybe (HRadical a)

Discrete types

data HDiscrete :: Hakaru -> * where

Concrete dictionaries for Hakaru types which are "discrete".

Constructors

HDiscrete_Nat :: HDiscrete HNat

HDiscrete_Int :: HDiscrete HInt

Instances

JmEq1 Hakaru HDiscrete

Methods

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

Eq1 Hakaru HDiscrete

Methods

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

Eq (HDiscrete a)

Methods

(==) :: HDiscrete a -> HDiscrete a -> Bool

(/=) :: HDiscrete a -> HDiscrete a -> Bool

Show (HDiscrete a)

Methods

showsPrec :: Int -> HDiscrete a -> ShowS

show :: HDiscrete a -> String

showList :: [HDiscrete a] -> ShowS

class HSemiring_ a => HDiscrete_ a where

Haskell type class for automatic HDiscrete inference.

Minimal complete definition

hDiscrete

Methods

hDiscrete :: HDiscrete a

Instances

HDiscrete_ HNat

Methods

hDiscrete :: HDiscrete HNat

HDiscrete_ HInt

Methods

hDiscrete :: HDiscrete HInt

sing_HDiscrete :: HDiscrete a -> Sing a

hDiscrete_Sing :: Sing a -> Maybe (HDiscrete a)

Continuous types

data HContinuous :: Hakaru -> * where

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 Hakaru HContinuous

Methods

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

Eq1 Hakaru HContinuous

Methods

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

Eq (HContinuous a)

Methods

(==) :: HContinuous a -> HContinuous a -> Bool

(/=) :: HContinuous a -> HContinuous a -> Bool

Show (HContinuous a)

Methods

showsPrec :: Int -> HContinuous a -> ShowS

show :: HContinuous a -> String

showList :: [HContinuous a] -> ShowS

hFractional_HContinuous :: HContinuous a -> HFractional a

Every HContinuous is a HFractional.

hSemiring_HIntegralContinuous :: HContinuous a -> HSemiring (HIntegral a)

The integral type of every HContinuous is a HSemiring.

class (HSemiring_ (HIntegral a), HFractional_ a) => HContinuous_ a where

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?

Minimal complete definition

hContinuous

Associated Types

type HIntegral (a :: Hakaru) :: Hakaru

Methods

hContinuous :: HContinuous a

Instances

HContinuous_ HProb

Associated Types

type HIntegral (HProb :: Hakaru) :: Hakaru

Methods

hContinuous :: HContinuous HProb

HContinuous_ HReal

Associated Types

type HIntegral (HReal :: Hakaru) :: Hakaru

Methods

hContinuous :: HContinuous HReal

sing_HContinuous :: HContinuous a -> Sing a

hContinuous_Sing :: Sing a -> Maybe (HContinuous a)

sing_HIntegral :: HContinuous a -> Sing (HIntegral a)