{-# LANGUAGE CPP
, GADTs
, KindSignatures
, DataKinds
, PolyKinds
, TypeFamilies
, FlexibleContexts
, FlexibleInstances
, TypeSynonymInstances
, StandaloneDeriving
#-}
{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
module Language.Hakaru.Types.HClasses
(
HEq(..)
, HEq_(..)
, sing_HEq
, hEq_Sing
, HOrd(..)
, hEq_HOrd
, HOrd_(..)
, sing_HOrd
, hOrd_Sing
, HIntegrable(..)
, sing_HIntegrable
, hIntegrable_Sing
, HSemiring(..)
, HSemiring_(..)
, sing_HSemiring
, hSemiring_Sing
, HRing(..)
, hSemiring_HRing
, hSemiring_NonNegativeHRing
, HRing_(..)
, sing_HRing
, hRing_Sing
, sing_NonNegative
, HFractional(..)
, hSemiring_HFractional
, HFractional_(..)
, sing_HFractional
, hFractional_Sing
, HRadical(..)
, hSemiring_HRadical
, HRadical_(..)
, sing_HRadical
, hRadical_Sing
, HDiscrete(..)
, HDiscrete_(..)
, sing_HDiscrete
, hDiscrete_Sing
, HContinuous(..)
, hFractional_HContinuous
, hSemiring_HIntegralContinuous
, HContinuous_(..)
, sing_HContinuous
, hContinuous_Sing
, sing_HIntegral
) where
#if __GLASGOW_HASKELL__ < 710
import Data.Functor ((<$>))
#endif
import Control.Applicative ((<|>), (<*>))
import Language.Hakaru.Syntax.IClasses (TypeEq(..), Eq1(..), JmEq1(..))
import Language.Hakaru.Types.DataKind
import Language.Hakaru.Types.Sing
import Control.Monad (join)
data HEq :: Hakaru -> * where
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)
deriving instance Eq (HEq a)
deriving instance Show (HEq a)
sing_HEq :: HEq a -> Sing a
sing_HEq :: HEq a -> Sing a
sing_HEq HEq a
HEq_Nat = Sing a
Sing 'HNat
SNat
sing_HEq HEq a
HEq_Int = Sing a
Sing 'HInt
SInt
sing_HEq HEq a
HEq_Prob = Sing a
Sing 'HProb
SProb
sing_HEq HEq a
HEq_Real = Sing a
Sing 'HReal
SReal
sing_HEq (HEq_Array HEq a
a) = Sing a -> Sing ('HArray a)
forall (a :: Hakaru). Sing a -> Sing ('HArray a)
SArray (HEq a -> Sing a
forall (a :: Hakaru). HEq a -> Sing a
sing_HEq HEq a
a)
sing_HEq HEq a
HEq_Bool = Sing a
Sing HBool
sBool
sing_HEq HEq a
HEq_Unit = Sing a
Sing HUnit
sUnit
sing_HEq (HEq_Pair HEq a
a HEq b
b) = Sing a -> Sing b -> Sing (HPair a b)
forall (a :: Hakaru) (b :: Hakaru).
Sing a -> Sing b -> Sing (HPair a b)
sPair (HEq a -> Sing a
forall (a :: Hakaru). HEq a -> Sing a
sing_HEq HEq a
a) (HEq b -> Sing b
forall (a :: Hakaru). HEq a -> Sing a
sing_HEq HEq b
b)
sing_HEq (HEq_Either HEq a
a HEq b
b) = Sing a -> Sing b -> Sing (HEither a b)
forall (a :: Hakaru) (b :: Hakaru).
Sing a -> Sing b -> Sing (HEither a b)
sEither (HEq a -> Sing a
forall (a :: Hakaru). HEq a -> Sing a
sing_HEq HEq a
a) (HEq b -> Sing b
forall (a :: Hakaru). HEq a -> Sing a
sing_HEq HEq b
b)
hEq_Sing :: Sing a -> Maybe (HEq a)
hEq_Sing :: Sing a -> Maybe (HEq a)
hEq_Sing Sing a
SNat = HEq 'HNat -> Maybe (HEq 'HNat)
forall a. a -> Maybe a
Just HEq 'HNat
HEq_Nat
hEq_Sing Sing a
SInt = HEq 'HInt -> Maybe (HEq 'HInt)
forall a. a -> Maybe a
Just HEq 'HInt
HEq_Int
hEq_Sing Sing a
SProb = HEq 'HProb -> Maybe (HEq 'HProb)
forall a. a -> Maybe a
Just HEq 'HProb
HEq_Prob
hEq_Sing Sing a
SReal = HEq 'HReal -> Maybe (HEq 'HReal)
forall a. a -> Maybe a
Just HEq 'HReal
HEq_Real
hEq_Sing (SArray a) = HEq a -> HEq ('HArray a)
forall (a :: Hakaru). HEq a -> HEq ('HArray a)
HEq_Array (HEq a -> HEq ('HArray a))
-> Maybe (HEq a) -> Maybe (HEq ('HArray a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sing a -> Maybe (HEq a)
forall (a :: Hakaru). Sing a -> Maybe (HEq a)
hEq_Sing Sing a
a
hEq_Sing Sing a
s =
(Sing a -> Sing HUnit -> Maybe (TypeEq a HUnit)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing a
s Sing HUnit
sUnit Maybe (TypeEq a HUnit)
-> (TypeEq a HUnit -> Maybe (HEq a)) -> Maybe (HEq a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq a HUnit
Refl -> HEq HUnit -> Maybe (HEq HUnit)
forall a. a -> Maybe a
Just HEq HUnit
HEq_Unit) Maybe (HEq a) -> Maybe (HEq a) -> Maybe (HEq a)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
(Sing a -> Sing HBool -> Maybe (TypeEq a HBool)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing a
s Sing HBool
sBool Maybe (TypeEq a HBool)
-> (TypeEq a HBool -> Maybe (HEq a)) -> Maybe (HEq a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq a HBool
Refl -> HEq HBool -> Maybe (HEq HBool)
forall a. a -> Maybe a
Just HEq HBool
HEq_Bool) Maybe (HEq a) -> Maybe (HEq a) -> Maybe (HEq a)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
(Maybe (Maybe (HEq a)) -> Maybe (HEq a)
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Maybe (Maybe (HEq a)) -> Maybe (HEq a))
-> Maybe (Maybe (HEq a)) -> Maybe (HEq a)
forall a b. (a -> b) -> a -> b
$ Sing a
-> (forall (a :: Hakaru) (b :: Hakaru).
(TypeEq a (HPair a b), Sing a, Sing b) -> Maybe (HEq a))
-> Maybe (Maybe (HEq a))
forall (x :: Hakaru) r.
Sing x
-> (forall (a :: Hakaru) (b :: Hakaru).
(TypeEq x (HPair a b), Sing a, Sing b) -> r)
-> Maybe r
sUnPair' Sing a
s ((forall (a :: Hakaru) (b :: Hakaru).
(TypeEq a (HPair a b), Sing a, Sing b) -> Maybe (HEq a))
-> Maybe (Maybe (HEq a)))
-> (forall (a :: Hakaru) (b :: Hakaru).
(TypeEq a (HPair a b), Sing a, Sing b) -> Maybe (HEq a))
-> Maybe (Maybe (HEq a))
forall a b. (a -> b) -> a -> b
$ \(TypeEq a (HPair a b)
Refl, Sing a
a, Sing b
b) ->
HEq a -> HEq b -> HEq (HPair a b)
forall (a :: Hakaru) (a :: Hakaru).
HEq a -> HEq a -> HEq (HPair a a)
HEq_Pair (HEq a -> HEq b -> HEq (HPair a b))
-> Maybe (HEq a) -> Maybe (HEq b -> HEq (HPair a b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sing a -> Maybe (HEq a)
forall (a :: Hakaru). Sing a -> Maybe (HEq a)
hEq_Sing Sing a
a Maybe (HEq b -> HEq (HPair a b))
-> Maybe (HEq b) -> Maybe (HEq (HPair a b))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Sing b -> Maybe (HEq b)
forall (a :: Hakaru). Sing a -> Maybe (HEq a)
hEq_Sing Sing b
b) Maybe (HEq a) -> Maybe (HEq a) -> Maybe (HEq a)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
(Maybe (Maybe (HEq a)) -> Maybe (HEq a)
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Maybe (Maybe (HEq a)) -> Maybe (HEq a))
-> Maybe (Maybe (HEq a)) -> Maybe (HEq a)
forall a b. (a -> b) -> a -> b
$ Sing a
-> (forall (a :: Hakaru) (b :: Hakaru).
(TypeEq a (HEither a b), Sing a, Sing b) -> Maybe (HEq a))
-> Maybe (Maybe (HEq a))
forall (x :: Hakaru) r.
Sing x
-> (forall (a :: Hakaru) (b :: Hakaru).
(TypeEq x (HEither a b), Sing a, Sing b) -> r)
-> Maybe r
sUnEither' Sing a
s ((forall (a :: Hakaru) (b :: Hakaru).
(TypeEq a (HEither a b), Sing a, Sing b) -> Maybe (HEq a))
-> Maybe (Maybe (HEq a)))
-> (forall (a :: Hakaru) (b :: Hakaru).
(TypeEq a (HEither a b), Sing a, Sing b) -> Maybe (HEq a))
-> Maybe (Maybe (HEq a))
forall a b. (a -> b) -> a -> b
$ \(TypeEq a (HEither a b)
Refl, Sing a
a, Sing b
b) ->
HEq a -> HEq b -> HEq (HEither a b)
forall (a :: Hakaru) (b :: Hakaru).
HEq a -> HEq b -> HEq (HEither a b)
HEq_Either (HEq a -> HEq b -> HEq (HEither a b))
-> Maybe (HEq a) -> Maybe (HEq b -> HEq (HEither a b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sing a -> Maybe (HEq a)
forall (a :: Hakaru). Sing a -> Maybe (HEq a)
hEq_Sing Sing a
a Maybe (HEq b -> HEq (HEither a b))
-> Maybe (HEq b) -> Maybe (HEq (HEither a b))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Sing b -> Maybe (HEq b)
forall (a :: Hakaru). Sing a -> Maybe (HEq a)
hEq_Sing Sing b
b)
class HEq_ (a :: Hakaru) where hEq :: HEq a
instance HEq_ 'HNat where hEq :: HEq 'HNat
hEq = HEq 'HNat
HEq_Nat
instance HEq_ 'HInt where hEq :: HEq 'HInt
hEq = HEq 'HInt
HEq_Int
instance HEq_ 'HProb where hEq :: HEq 'HProb
hEq = HEq 'HProb
HEq_Prob
instance HEq_ 'HReal where hEq :: HEq 'HReal
hEq = HEq 'HReal
HEq_Real
instance HEq_ HBool where hEq :: HEq HBool
hEq = HEq HBool
HEq_Bool
instance HEq_ HUnit where hEq :: HEq HUnit
hEq = HEq HUnit
HEq_Unit
instance (HEq_ a) => HEq_ ('HArray a) where
hEq :: HEq ('HArray a)
hEq = HEq a -> HEq ('HArray a)
forall (a :: Hakaru). HEq a -> HEq ('HArray a)
HEq_Array HEq a
forall (a :: Hakaru). HEq_ a => HEq a
hEq
instance (HEq_ a, HEq_ b) => HEq_ (HPair a b) where
hEq :: HEq (HPair a b)
hEq = HEq a -> HEq b -> HEq (HPair a b)
forall (a :: Hakaru) (a :: Hakaru).
HEq a -> HEq a -> HEq (HPair a a)
HEq_Pair HEq a
forall (a :: Hakaru). HEq_ a => HEq a
hEq HEq b
forall (a :: Hakaru). HEq_ a => HEq a
hEq
instance (HEq_ a, HEq_ b) => HEq_ (HEither a b) where
hEq :: HEq (HEither a b)
hEq = HEq a -> HEq b -> HEq (HEither a b)
forall (a :: Hakaru) (b :: Hakaru).
HEq a -> HEq b -> HEq (HEither a b)
HEq_Either HEq a
forall (a :: Hakaru). HEq_ a => HEq a
hEq HEq b
forall (a :: Hakaru). HEq_ a => HEq a
hEq
data HOrd :: Hakaru -> * where
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)
deriving instance Eq (HOrd a)
deriving instance Show (HOrd a)
sing_HOrd :: HOrd a -> Sing a
sing_HOrd :: HOrd a -> Sing a
sing_HOrd HOrd a
HOrd_Nat = Sing a
Sing 'HNat
SNat
sing_HOrd HOrd a
HOrd_Int = Sing a
Sing 'HInt
SInt
sing_HOrd HOrd a
HOrd_Prob = Sing a
Sing 'HProb
SProb
sing_HOrd HOrd a
HOrd_Real = Sing a
Sing 'HReal
SReal
sing_HOrd (HOrd_Array HOrd a
a) = Sing a -> Sing ('HArray a)
forall (a :: Hakaru). Sing a -> Sing ('HArray a)
SArray (HOrd a -> Sing a
forall (a :: Hakaru). HOrd a -> Sing a
sing_HOrd HOrd a
a)
sing_HOrd HOrd a
HOrd_Bool = Sing a
Sing HBool
sBool
sing_HOrd HOrd a
HOrd_Unit = Sing a
Sing HUnit
sUnit
sing_HOrd (HOrd_Pair HOrd a
a HOrd b
b) = Sing a -> Sing b -> Sing (HPair a b)
forall (a :: Hakaru) (b :: Hakaru).
Sing a -> Sing b -> Sing (HPair a b)
sPair (HOrd a -> Sing a
forall (a :: Hakaru). HOrd a -> Sing a
sing_HOrd HOrd a
a) (HOrd b -> Sing b
forall (a :: Hakaru). HOrd a -> Sing a
sing_HOrd HOrd b
b)
sing_HOrd (HOrd_Either HOrd a
a HOrd b
b) = Sing a -> Sing b -> Sing (HEither a b)
forall (a :: Hakaru) (b :: Hakaru).
Sing a -> Sing b -> Sing (HEither a b)
sEither (HOrd a -> Sing a
forall (a :: Hakaru). HOrd a -> Sing a
sing_HOrd HOrd a
a) (HOrd b -> Sing b
forall (a :: Hakaru). HOrd a -> Sing a
sing_HOrd HOrd b
b)
hOrd_Sing :: Sing a -> Maybe (HOrd a)
hOrd_Sing :: Sing a -> Maybe (HOrd a)
hOrd_Sing Sing a
SNat = HOrd 'HNat -> Maybe (HOrd 'HNat)
forall a. a -> Maybe a
Just HOrd 'HNat
HOrd_Nat
hOrd_Sing Sing a
SInt = HOrd 'HInt -> Maybe (HOrd 'HInt)
forall a. a -> Maybe a
Just HOrd 'HInt
HOrd_Int
hOrd_Sing Sing a
SProb = HOrd 'HProb -> Maybe (HOrd 'HProb)
forall a. a -> Maybe a
Just HOrd 'HProb
HOrd_Prob
hOrd_Sing Sing a
SReal = HOrd 'HReal -> Maybe (HOrd 'HReal)
forall a. a -> Maybe a
Just HOrd 'HReal
HOrd_Real
hOrd_Sing (SArray a) = HOrd a -> HOrd ('HArray a)
forall (a :: Hakaru). HOrd a -> HOrd ('HArray a)
HOrd_Array (HOrd a -> HOrd ('HArray a))
-> Maybe (HOrd a) -> Maybe (HOrd ('HArray a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sing a -> Maybe (HOrd a)
forall (a :: Hakaru). Sing a -> Maybe (HOrd a)
hOrd_Sing Sing a
a
hOrd_Sing Sing a
_ = Maybe (HOrd a)
forall a. Maybe a
Nothing
hEq_HOrd :: HOrd a -> HEq a
hEq_HOrd :: HOrd a -> HEq a
hEq_HOrd HOrd a
HOrd_Nat = HEq a
HEq 'HNat
HEq_Nat
hEq_HOrd HOrd a
HOrd_Int = HEq a
HEq 'HInt
HEq_Int
hEq_HOrd HOrd a
HOrd_Prob = HEq a
HEq 'HProb
HEq_Prob
hEq_HOrd HOrd a
HOrd_Real = HEq a
HEq 'HReal
HEq_Real
hEq_HOrd (HOrd_Array HOrd a
a) = HEq a -> HEq ('HArray a)
forall (a :: Hakaru). HEq a -> HEq ('HArray a)
HEq_Array (HOrd a -> HEq a
forall (a :: Hakaru). HOrd a -> HEq a
hEq_HOrd HOrd a
a)
hEq_HOrd HOrd a
HOrd_Bool = HEq a
HEq HBool
HEq_Bool
hEq_HOrd HOrd a
HOrd_Unit = HEq a
HEq HUnit
HEq_Unit
hEq_HOrd (HOrd_Pair HOrd a
a HOrd b
b) = HEq a -> HEq b -> HEq (HPair a b)
forall (a :: Hakaru) (a :: Hakaru).
HEq a -> HEq a -> HEq (HPair a a)
HEq_Pair (HOrd a -> HEq a
forall (a :: Hakaru). HOrd a -> HEq a
hEq_HOrd HOrd a
a) (HOrd b -> HEq b
forall (a :: Hakaru). HOrd a -> HEq a
hEq_HOrd HOrd b
b)
hEq_HOrd (HOrd_Either HOrd a
a HOrd b
b) = HEq a -> HEq b -> HEq (HEither a b)
forall (a :: Hakaru) (b :: Hakaru).
HEq a -> HEq b -> HEq (HEither a b)
HEq_Either (HOrd a -> HEq a
forall (a :: Hakaru). HOrd a -> HEq a
hEq_HOrd HOrd a
a) (HOrd b -> HEq b
forall (a :: Hakaru). HOrd a -> HEq a
hEq_HOrd HOrd b
b)
class HEq_ a => HOrd_ (a :: Hakaru) where hOrd :: HOrd a
instance HOrd_ 'HNat where hOrd :: HOrd 'HNat
hOrd = HOrd 'HNat
HOrd_Nat
instance HOrd_ 'HInt where hOrd :: HOrd 'HInt
hOrd = HOrd 'HInt
HOrd_Int
instance HOrd_ 'HProb where hOrd :: HOrd 'HProb
hOrd = HOrd 'HProb
HOrd_Prob
instance HOrd_ 'HReal where hOrd :: HOrd 'HReal
hOrd = HOrd 'HReal
HOrd_Real
instance HOrd_ HBool where hOrd :: HOrd HBool
hOrd = HOrd HBool
HOrd_Bool
instance HOrd_ HUnit where hOrd :: HOrd HUnit
hOrd = HOrd HUnit
HOrd_Unit
instance (HOrd_ a) => HOrd_ ('HArray a) where
hOrd :: HOrd ('HArray a)
hOrd = HOrd a -> HOrd ('HArray a)
forall (a :: Hakaru). HOrd a -> HOrd ('HArray a)
HOrd_Array HOrd a
forall (a :: Hakaru). HOrd_ a => HOrd a
hOrd
instance (HOrd_ a, HOrd_ b) => HOrd_ (HPair a b) where
hOrd :: HOrd (HPair a b)
hOrd = HOrd a -> HOrd b -> HOrd (HPair a b)
forall (a :: Hakaru) (a :: Hakaru).
HOrd a -> HOrd a -> HOrd (HPair a a)
HOrd_Pair HOrd a
forall (a :: Hakaru). HOrd_ a => HOrd a
hOrd HOrd b
forall (a :: Hakaru). HOrd_ a => HOrd a
hOrd
instance (HOrd_ a, HOrd_ b) => HOrd_ (HEither a b) where
hOrd :: HOrd (HEither a b)
hOrd = HOrd a -> HOrd b -> HOrd (HEither a b)
forall (a :: Hakaru) (b :: Hakaru).
HOrd a -> HOrd b -> HOrd (HEither a b)
HOrd_Either HOrd a
forall (a :: Hakaru). HOrd_ a => HOrd a
hOrd HOrd b
forall (a :: Hakaru). HOrd_ a => HOrd a
hOrd
data HSemiring :: Hakaru -> * where
HSemiring_Nat :: HSemiring 'HNat
HSemiring_Int :: HSemiring 'HInt
HSemiring_Prob :: HSemiring 'HProb
HSemiring_Real :: HSemiring 'HReal
instance Eq (HSemiring a) where
== :: HSemiring a -> HSemiring a -> Bool
(==) = HSemiring a -> HSemiring a -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1
instance Eq1 HSemiring where
eq1 :: HSemiring i -> HSemiring i -> Bool
eq1 HSemiring i
x HSemiring i
y = Bool -> (TypeEq i i -> Bool) -> Maybe (TypeEq i i) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Bool -> TypeEq i i -> Bool
forall a b. a -> b -> a
const Bool
True) (HSemiring i -> HSemiring i -> Maybe (TypeEq i i)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 HSemiring i
x HSemiring i
y)
instance JmEq1 HSemiring where
jmEq1 :: HSemiring i -> HSemiring j -> Maybe (TypeEq i j)
jmEq1 HSemiring i
HSemiring_Nat HSemiring j
HSemiring_Nat = TypeEq i i -> Maybe (TypeEq i i)
forall a. a -> Maybe a
Just TypeEq i i
forall k (a :: k). TypeEq a a
Refl
jmEq1 HSemiring i
HSemiring_Int HSemiring j
HSemiring_Int = TypeEq i i -> Maybe (TypeEq i i)
forall a. a -> Maybe a
Just TypeEq i i
forall k (a :: k). TypeEq a a
Refl
jmEq1 HSemiring i
HSemiring_Prob HSemiring j
HSemiring_Prob = TypeEq i i -> Maybe (TypeEq i i)
forall a. a -> Maybe a
Just TypeEq i i
forall k (a :: k). TypeEq a a
Refl
jmEq1 HSemiring i
HSemiring_Real HSemiring j
HSemiring_Real = TypeEq i i -> Maybe (TypeEq i i)
forall a. a -> Maybe a
Just TypeEq i i
forall k (a :: k). TypeEq a a
Refl
jmEq1 HSemiring i
_ HSemiring j
_ = Maybe (TypeEq i j)
forall a. Maybe a
Nothing
deriving instance Show (HSemiring a)
sing_HSemiring :: HSemiring a -> Sing a
sing_HSemiring :: HSemiring a -> Sing a
sing_HSemiring HSemiring a
HSemiring_Nat = Sing a
Sing 'HNat
SNat
sing_HSemiring HSemiring a
HSemiring_Int = Sing a
Sing 'HInt
SInt
sing_HSemiring HSemiring a
HSemiring_Prob = Sing a
Sing 'HProb
SProb
sing_HSemiring HSemiring a
HSemiring_Real = Sing a
Sing 'HReal
SReal
hSemiring_Sing :: Sing a -> Maybe (HSemiring a)
hSemiring_Sing :: Sing a -> Maybe (HSemiring a)
hSemiring_Sing Sing a
SNat = HSemiring 'HNat -> Maybe (HSemiring 'HNat)
forall a. a -> Maybe a
Just HSemiring 'HNat
HSemiring_Nat
hSemiring_Sing Sing a
SInt = HSemiring 'HInt -> Maybe (HSemiring 'HInt)
forall a. a -> Maybe a
Just HSemiring 'HInt
HSemiring_Int
hSemiring_Sing Sing a
SProb = HSemiring 'HProb -> Maybe (HSemiring 'HProb)
forall a. a -> Maybe a
Just HSemiring 'HProb
HSemiring_Prob
hSemiring_Sing Sing a
SReal = HSemiring 'HReal -> Maybe (HSemiring 'HReal)
forall a. a -> Maybe a
Just HSemiring 'HReal
HSemiring_Real
hSemiring_Sing Sing a
_ = Maybe (HSemiring a)
forall a. Maybe a
Nothing
class HSemiring_ (a :: Hakaru) where hSemiring :: HSemiring a
instance HSemiring_ 'HNat where hSemiring :: HSemiring 'HNat
hSemiring = HSemiring 'HNat
HSemiring_Nat
instance HSemiring_ 'HInt where hSemiring :: HSemiring 'HInt
hSemiring = HSemiring 'HInt
HSemiring_Int
instance HSemiring_ 'HProb where hSemiring :: HSemiring 'HProb
hSemiring = HSemiring 'HProb
HSemiring_Prob
instance HSemiring_ 'HReal where hSemiring :: HSemiring 'HReal
hSemiring = HSemiring 'HReal
HSemiring_Real
data HRing :: Hakaru -> * where
HRing_Int :: HRing 'HInt
HRing_Real :: HRing 'HReal
instance Eq (HRing a) where
== :: HRing a -> HRing a -> Bool
(==) = HRing a -> HRing a -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1
instance Eq1 HRing where
eq1 :: HRing i -> HRing i -> Bool
eq1 HRing i
x HRing i
y = Bool -> (TypeEq i i -> Bool) -> Maybe (TypeEq i i) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Bool -> TypeEq i i -> Bool
forall a b. a -> b -> a
const Bool
True) (HRing i -> HRing i -> Maybe (TypeEq i i)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 HRing i
x HRing i
y)
instance JmEq1 HRing where
jmEq1 :: HRing i -> HRing j -> Maybe (TypeEq i j)
jmEq1 HRing i
HRing_Int HRing j
HRing_Int = TypeEq i i -> Maybe (TypeEq i i)
forall a. a -> Maybe a
Just TypeEq i i
forall k (a :: k). TypeEq a a
Refl
jmEq1 HRing i
HRing_Real HRing j
HRing_Real = TypeEq i i -> Maybe (TypeEq i i)
forall a. a -> Maybe a
Just TypeEq i i
forall k (a :: k). TypeEq a a
Refl
jmEq1 HRing i
_ HRing j
_ = Maybe (TypeEq i j)
forall a. Maybe a
Nothing
deriving instance Show (HRing a)
sing_HRing :: HRing a -> Sing a
sing_HRing :: HRing a -> Sing a
sing_HRing HRing a
HRing_Int = Sing a
Sing 'HInt
SInt
sing_HRing HRing a
HRing_Real = Sing a
Sing 'HReal
SReal
hRing_Sing :: Sing a -> Maybe (HRing a)
hRing_Sing :: Sing a -> Maybe (HRing a)
hRing_Sing Sing a
SInt = HRing 'HInt -> Maybe (HRing 'HInt)
forall a. a -> Maybe a
Just HRing 'HInt
HRing_Int
hRing_Sing Sing a
SReal = HRing 'HReal -> Maybe (HRing 'HReal)
forall a. a -> Maybe a
Just HRing 'HReal
HRing_Real
hRing_Sing Sing a
_ = Maybe (HRing a)
forall a. Maybe a
Nothing
sing_NonNegative :: HRing a -> Sing (NonNegative a)
sing_NonNegative :: HRing a -> Sing (NonNegative a)
sing_NonNegative = HSemiring (NonNegative a) -> Sing (NonNegative a)
forall (a :: Hakaru). HSemiring a -> Sing a
sing_HSemiring (HSemiring (NonNegative a) -> Sing (NonNegative a))
-> (HRing a -> HSemiring (NonNegative a))
-> HRing a
-> Sing (NonNegative a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HRing a -> HSemiring (NonNegative a)
forall (a :: Hakaru). HRing a -> HSemiring (NonNegative a)
hSemiring_NonNegativeHRing
hSemiring_HRing :: HRing a -> HSemiring a
hSemiring_HRing :: HRing a -> HSemiring a
hSemiring_HRing HRing a
HRing_Int = HSemiring a
HSemiring 'HInt
HSemiring_Int
hSemiring_HRing HRing a
HRing_Real = HSemiring a
HSemiring 'HReal
HSemiring_Real
hSemiring_NonNegativeHRing :: HRing a -> HSemiring (NonNegative a)
hSemiring_NonNegativeHRing :: HRing a -> HSemiring (NonNegative a)
hSemiring_NonNegativeHRing HRing a
HRing_Int = HSemiring 'HNat
HSemiring (NonNegative a)
HSemiring_Nat
hSemiring_NonNegativeHRing HRing a
HRing_Real = HSemiring 'HProb
HSemiring (NonNegative a)
HSemiring_Prob
class (HSemiring_ (NonNegative a), HSemiring_ a) => HRing_ (a :: Hakaru)
where
type NonNegative (a :: Hakaru) :: Hakaru
hRing :: HRing a
instance HRing_ 'HInt where
type NonNegative 'HInt = 'HNat
hRing :: HRing 'HInt
hRing = HRing 'HInt
HRing_Int
instance HRing_ 'HReal where
type NonNegative 'HReal = 'HProb
hRing :: HRing 'HReal
hRing = HRing 'HReal
HRing_Real
data HFractional :: Hakaru -> * where
HFractional_Prob :: HFractional 'HProb
HFractional_Real :: HFractional 'HReal
instance Eq (HFractional a) where
== :: HFractional a -> HFractional a -> Bool
(==) = HFractional a -> HFractional a -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1
instance Eq1 HFractional where
eq1 :: HFractional i -> HFractional i -> Bool
eq1 HFractional i
x HFractional i
y = Bool -> (TypeEq i i -> Bool) -> Maybe (TypeEq i i) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Bool -> TypeEq i i -> Bool
forall a b. a -> b -> a
const Bool
True) (HFractional i -> HFractional i -> Maybe (TypeEq i i)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 HFractional i
x HFractional i
y)
instance JmEq1 HFractional where
jmEq1 :: HFractional i -> HFractional j -> Maybe (TypeEq i j)
jmEq1 HFractional i
HFractional_Prob HFractional j
HFractional_Prob = TypeEq i i -> Maybe (TypeEq i i)
forall a. a -> Maybe a
Just TypeEq i i
forall k (a :: k). TypeEq a a
Refl
jmEq1 HFractional i
HFractional_Real HFractional j
HFractional_Real = TypeEq i i -> Maybe (TypeEq i i)
forall a. a -> Maybe a
Just TypeEq i i
forall k (a :: k). TypeEq a a
Refl
jmEq1 HFractional i
_ HFractional j
_ = Maybe (TypeEq i j)
forall a. Maybe a
Nothing
deriving instance Show (HFractional a)
sing_HFractional :: HFractional a -> Sing a
sing_HFractional :: HFractional a -> Sing a
sing_HFractional HFractional a
HFractional_Prob = Sing a
Sing 'HProb
SProb
sing_HFractional HFractional a
HFractional_Real = Sing a
Sing 'HReal
SReal
hFractional_Sing :: Sing a -> Maybe (HFractional a)
hFractional_Sing :: Sing a -> Maybe (HFractional a)
hFractional_Sing Sing a
SProb = HFractional 'HProb -> Maybe (HFractional 'HProb)
forall a. a -> Maybe a
Just HFractional 'HProb
HFractional_Prob
hFractional_Sing Sing a
SReal = HFractional 'HReal -> Maybe (HFractional 'HReal)
forall a. a -> Maybe a
Just HFractional 'HReal
HFractional_Real
hFractional_Sing Sing a
_ = Maybe (HFractional a)
forall a. Maybe a
Nothing
hSemiring_HFractional :: HFractional a -> HSemiring a
hSemiring_HFractional :: HFractional a -> HSemiring a
hSemiring_HFractional HFractional a
HFractional_Prob = HSemiring a
HSemiring 'HProb
HSemiring_Prob
hSemiring_HFractional HFractional a
HFractional_Real = HSemiring a
HSemiring 'HReal
HSemiring_Real
class (HSemiring_ a) => HFractional_ (a :: Hakaru) where
hFractional :: HFractional a
instance HFractional_ 'HProb where hFractional :: HFractional 'HProb
hFractional = HFractional 'HProb
HFractional_Prob
instance HFractional_ 'HReal where hFractional :: HFractional 'HReal
hFractional = HFractional 'HReal
HFractional_Real
data HRadical :: Hakaru -> * where
HRadical_Prob :: HRadical 'HProb
instance Eq (HRadical a) where
== :: HRadical a -> HRadical a -> Bool
(==) = HRadical a -> HRadical a -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1
instance Eq1 HRadical where
eq1 :: HRadical i -> HRadical i -> Bool
eq1 HRadical i
x HRadical i
y = Bool -> (TypeEq i i -> Bool) -> Maybe (TypeEq i i) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Bool -> TypeEq i i -> Bool
forall a b. a -> b -> a
const Bool
True) (HRadical i -> HRadical i -> Maybe (TypeEq i i)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 HRadical i
x HRadical i
y)
instance JmEq1 HRadical where
jmEq1 :: HRadical i -> HRadical j -> Maybe (TypeEq i j)
jmEq1 HRadical i
HRadical_Prob HRadical j
HRadical_Prob = TypeEq i i -> Maybe (TypeEq i i)
forall a. a -> Maybe a
Just TypeEq i i
forall k (a :: k). TypeEq a a
Refl
deriving instance Show (HRadical a)
sing_HRadical :: HRadical a -> Sing a
sing_HRadical :: HRadical a -> Sing a
sing_HRadical HRadical a
HRadical_Prob = Sing a
Sing 'HProb
SProb
hRadical_Sing :: Sing a -> Maybe (HRadical a)
hRadical_Sing :: Sing a -> Maybe (HRadical a)
hRadical_Sing Sing a
SProb = HRadical 'HProb -> Maybe (HRadical 'HProb)
forall a. a -> Maybe a
Just HRadical 'HProb
HRadical_Prob
hRadical_Sing Sing a
_ = Maybe (HRadical a)
forall a. Maybe a
Nothing
hSemiring_HRadical :: HRadical a -> HSemiring a
hSemiring_HRadical :: HRadical a -> HSemiring a
hSemiring_HRadical HRadical a
HRadical_Prob = HSemiring a
HSemiring 'HProb
HSemiring_Prob
class (HSemiring_ a) => HRadical_ (a :: Hakaru) where
hRadical :: HRadical a
instance HRadical_ 'HProb where hRadical :: HRadical 'HProb
hRadical = HRadical 'HProb
HRadical_Prob
data HIntegrable :: Hakaru -> * where
HIntegrable_Nat :: HIntegrable 'HNat
HIntegrable_Prob :: HIntegrable 'HProb
instance Eq (HIntegrable a) where
== :: HIntegrable a -> HIntegrable a -> Bool
(==) = HIntegrable a -> HIntegrable a -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1
instance Eq1 HIntegrable where
eq1 :: HIntegrable i -> HIntegrable i -> Bool
eq1 HIntegrable i
x HIntegrable i
y = Bool -> (TypeEq i i -> Bool) -> Maybe (TypeEq i i) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Bool -> TypeEq i i -> Bool
forall a b. a -> b -> a
const Bool
True) (HIntegrable i -> HIntegrable i -> Maybe (TypeEq i i)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 HIntegrable i
x HIntegrable i
y)
instance JmEq1 HIntegrable where
jmEq1 :: HIntegrable i -> HIntegrable j -> Maybe (TypeEq i j)
jmEq1 HIntegrable i
HIntegrable_Nat HIntegrable j
HIntegrable_Nat = TypeEq i i -> Maybe (TypeEq i i)
forall a. a -> Maybe a
Just TypeEq i i
forall k (a :: k). TypeEq a a
Refl
jmEq1 HIntegrable i
HIntegrable_Prob HIntegrable j
HIntegrable_Prob = TypeEq i i -> Maybe (TypeEq i i)
forall a. a -> Maybe a
Just TypeEq i i
forall k (a :: k). TypeEq a a
Refl
jmEq1 HIntegrable i
_ HIntegrable j
_ = Maybe (TypeEq i j)
forall a. Maybe a
Nothing
deriving instance Show (HIntegrable a)
sing_HIntegrable :: HIntegrable a -> Sing a
sing_HIntegrable :: HIntegrable a -> Sing a
sing_HIntegrable HIntegrable a
HIntegrable_Nat = Sing a
Sing 'HNat
SNat
sing_HIntegrable HIntegrable a
HIntegrable_Prob = Sing a
Sing 'HProb
SProb
hIntegrable_Sing :: Sing a -> Maybe (HIntegrable a)
hIntegrable_Sing :: Sing a -> Maybe (HIntegrable a)
hIntegrable_Sing Sing a
SNat = HIntegrable 'HNat -> Maybe (HIntegrable 'HNat)
forall a. a -> Maybe a
Just HIntegrable 'HNat
HIntegrable_Nat
hIntegrable_Sing Sing a
SProb = HIntegrable 'HProb -> Maybe (HIntegrable 'HProb)
forall a. a -> Maybe a
Just HIntegrable 'HProb
HIntegrable_Prob
hIntegrable_Sing Sing a
_ = Maybe (HIntegrable a)
forall a. Maybe a
Nothing
data HDiscrete :: Hakaru -> * where
HDiscrete_Nat :: HDiscrete 'HNat
HDiscrete_Int :: HDiscrete 'HInt
instance Eq (HDiscrete a) where
== :: HDiscrete a -> HDiscrete a -> Bool
(==) = HDiscrete a -> HDiscrete a -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1
instance Eq1 HDiscrete where
eq1 :: HDiscrete i -> HDiscrete i -> Bool
eq1 HDiscrete i
x HDiscrete i
y = Bool -> (TypeEq i i -> Bool) -> Maybe (TypeEq i i) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Bool -> TypeEq i i -> Bool
forall a b. a -> b -> a
const Bool
True) (HDiscrete i -> HDiscrete i -> Maybe (TypeEq i i)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 HDiscrete i
x HDiscrete i
y)
instance JmEq1 HDiscrete where
jmEq1 :: HDiscrete i -> HDiscrete j -> Maybe (TypeEq i j)
jmEq1 HDiscrete i
HDiscrete_Nat HDiscrete j
HDiscrete_Nat = TypeEq i i -> Maybe (TypeEq i i)
forall a. a -> Maybe a
Just TypeEq i i
forall k (a :: k). TypeEq a a
Refl
jmEq1 HDiscrete i
HDiscrete_Int HDiscrete j
HDiscrete_Int = TypeEq i i -> Maybe (TypeEq i i)
forall a. a -> Maybe a
Just TypeEq i i
forall k (a :: k). TypeEq a a
Refl
jmEq1 HDiscrete i
_ HDiscrete j
_ = Maybe (TypeEq i j)
forall a. Maybe a
Nothing
deriving instance Show (HDiscrete a)
sing_HDiscrete :: HDiscrete a -> Sing a
sing_HDiscrete :: HDiscrete a -> Sing a
sing_HDiscrete HDiscrete a
HDiscrete_Nat = Sing a
Sing 'HNat
SNat
sing_HDiscrete HDiscrete a
HDiscrete_Int = Sing a
Sing 'HInt
SInt
hDiscrete_Sing :: Sing a -> Maybe (HDiscrete a)
hDiscrete_Sing :: Sing a -> Maybe (HDiscrete a)
hDiscrete_Sing Sing a
SNat = HDiscrete 'HNat -> Maybe (HDiscrete 'HNat)
forall a. a -> Maybe a
Just HDiscrete 'HNat
HDiscrete_Nat
hDiscrete_Sing Sing a
SInt = HDiscrete 'HInt -> Maybe (HDiscrete 'HInt)
forall a. a -> Maybe a
Just HDiscrete 'HInt
HDiscrete_Int
hDiscrete_Sing Sing a
_ = Maybe (HDiscrete a)
forall a. Maybe a
Nothing
class (HSemiring_ a) => HDiscrete_ (a :: Hakaru) where
hDiscrete :: HDiscrete a
instance HDiscrete_ 'HNat where hDiscrete :: HDiscrete 'HNat
hDiscrete = HDiscrete 'HNat
HDiscrete_Nat
instance HDiscrete_ 'HInt where hDiscrete :: HDiscrete 'HInt
hDiscrete = HDiscrete 'HInt
HDiscrete_Int
data HContinuous :: Hakaru -> * where
HContinuous_Prob :: HContinuous 'HProb
HContinuous_Real :: HContinuous 'HReal
instance Eq (HContinuous a) where
== :: HContinuous a -> HContinuous a -> Bool
(==) = HContinuous a -> HContinuous a -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1
instance Eq1 HContinuous where
eq1 :: HContinuous i -> HContinuous i -> Bool
eq1 HContinuous i
x HContinuous i
y = Bool -> (TypeEq i i -> Bool) -> Maybe (TypeEq i i) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Bool -> TypeEq i i -> Bool
forall a b. a -> b -> a
const Bool
True) (HContinuous i -> HContinuous i -> Maybe (TypeEq i i)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 HContinuous i
x HContinuous i
y)
instance JmEq1 HContinuous where
jmEq1 :: HContinuous i -> HContinuous j -> Maybe (TypeEq i j)
jmEq1 HContinuous i
HContinuous_Prob HContinuous j
HContinuous_Prob = TypeEq i i -> Maybe (TypeEq i i)
forall a. a -> Maybe a
Just TypeEq i i
forall k (a :: k). TypeEq a a
Refl
jmEq1 HContinuous i
HContinuous_Real HContinuous j
HContinuous_Real = TypeEq i i -> Maybe (TypeEq i i)
forall a. a -> Maybe a
Just TypeEq i i
forall k (a :: k). TypeEq a a
Refl
jmEq1 HContinuous i
_ HContinuous j
_ = Maybe (TypeEq i j)
forall a. Maybe a
Nothing
deriving instance Show (HContinuous a)
sing_HContinuous :: HContinuous a -> Sing a
sing_HContinuous :: HContinuous a -> Sing a
sing_HContinuous HContinuous a
HContinuous_Prob = Sing a
Sing 'HProb
SProb
sing_HContinuous HContinuous a
HContinuous_Real = Sing a
Sing 'HReal
SReal
hContinuous_Sing :: Sing a -> Maybe (HContinuous a)
hContinuous_Sing :: Sing a -> Maybe (HContinuous a)
hContinuous_Sing Sing a
SProb = HContinuous 'HProb -> Maybe (HContinuous 'HProb)
forall a. a -> Maybe a
Just HContinuous 'HProb
HContinuous_Prob
hContinuous_Sing Sing a
SReal = HContinuous 'HReal -> Maybe (HContinuous 'HReal)
forall a. a -> Maybe a
Just HContinuous 'HReal
HContinuous_Real
hContinuous_Sing Sing a
_ = Maybe (HContinuous a)
forall a. Maybe a
Nothing
sing_HIntegral :: HContinuous a -> Sing (HIntegral a)
sing_HIntegral :: HContinuous a -> Sing (HIntegral a)
sing_HIntegral = HSemiring (HIntegral a) -> Sing (HIntegral a)
forall (a :: Hakaru). HSemiring a -> Sing a
sing_HSemiring (HSemiring (HIntegral a) -> Sing (HIntegral a))
-> (HContinuous a -> HSemiring (HIntegral a))
-> HContinuous a
-> Sing (HIntegral a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HContinuous a -> HSemiring (HIntegral a)
forall (a :: Hakaru). HContinuous a -> HSemiring (HIntegral a)
hSemiring_HIntegralContinuous
hFractional_HContinuous :: HContinuous a -> HFractional a
hFractional_HContinuous :: HContinuous a -> HFractional a
hFractional_HContinuous HContinuous a
HContinuous_Prob = HFractional a
HFractional 'HProb
HFractional_Prob
hFractional_HContinuous HContinuous a
HContinuous_Real = HFractional a
HFractional 'HReal
HFractional_Real
hSemiring_HIntegralContinuous :: HContinuous a -> HSemiring (HIntegral a)
hSemiring_HIntegralContinuous :: HContinuous a -> HSemiring (HIntegral a)
hSemiring_HIntegralContinuous HContinuous a
HContinuous_Prob = HSemiring 'HNat
HSemiring (HIntegral a)
HSemiring_Nat
hSemiring_HIntegralContinuous HContinuous a
HContinuous_Real = HSemiring 'HInt
HSemiring (HIntegral a)
HSemiring_Int
class (HSemiring_ (HIntegral a), HFractional_ a)
=> HContinuous_ (a :: Hakaru)
where
type HIntegral (a :: Hakaru) :: Hakaru
hContinuous :: HContinuous a
instance HContinuous_ 'HProb where
type HIntegral 'HProb = 'HNat
hContinuous :: HContinuous 'HProb
hContinuous = HContinuous 'HProb
HContinuous_Prob
instance HContinuous_ 'HReal where
type HIntegral 'HReal = 'HInt
hContinuous :: HContinuous 'HReal
hContinuous = HContinuous 'HReal
HContinuous_Real