{-# LANGUAGE CPP
           , GADTs
           , KindSignatures
           , DataKinds
           , PolyKinds
           , TypeFamilies
           , FlexibleContexts
           , FlexibleInstances
           , TypeSynonymInstances
           , StandaloneDeriving
           #-}

{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
----------------------------------------------------------------
--                                                    2015.12.15
-- |
-- Module      :  Language.Hakaru.Types.HClasses
-- Copyright   :  Copyright (c) 2016 the Hakaru team
-- License     :  BSD3
-- Maintainer  :  wren@community.haskell.org
-- Stability   :  experimental
-- Portability :  GHC-only
--
-- A collection of type classes for encoding Hakaru's numeric hierarchy.
----------------------------------------------------------------
module Language.Hakaru.Types.HClasses
    (
    -- * Equality
      HEq(..)
    , HEq_(..)
    , sing_HEq
    , hEq_Sing

    -- * Ordering
    , HOrd(..)
    , hEq_HOrd
    , HOrd_(..)
    , sing_HOrd
    , hOrd_Sing

   -- * HIntegrable
    , HIntegrable(..)
    , sing_HIntegrable
    , hIntegrable_Sing

    -- * Semirings
    , HSemiring(..)
    , HSemiring_(..)
    , sing_HSemiring
    , hSemiring_Sing

    -- * Rings
    , HRing(..)
    , hSemiring_HRing
    , hSemiring_NonNegativeHRing
    , HRing_(..)
    , sing_HRing
    , hRing_Sing
    , sing_NonNegative

    -- * Fractional types
    , HFractional(..)
    , hSemiring_HFractional
    , HFractional_(..)
    , sing_HFractional
    , hFractional_Sing

    -- * Radical types
    , HRadical(..)
    , hSemiring_HRadical
    , HRadical_(..)
    , sing_HRadical
    , hRadical_Sing

   -- * Discrete types
    , HDiscrete(..)
    , HDiscrete_(..)
    , sing_HDiscrete
    , hDiscrete_Sing

    -- * Continuous types
    , 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)

----------------------------------------------------------------
-- | Concrete dictionaries for Hakaru types with decidable equality.
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)
-- TODO: instance JmEq1 HEq
-- BUG: deriving instance Read (HEq a)
deriving instance Show (HEq a)

-- N.B., we do case analysis so that we don't need the class constraint!
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)

-- | Haskell type class for automatic 'HEq' inference.
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


----------------------------------------------------------------
-- | Concrete dictionaries for Hakaru types with decidable total ordering.
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)
-- TODO: instance JmEq1 HOrd
-- BUG: deriving instance Read (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

-- | Every 'HOrd' type is 'HEq'.
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)

-- | Haskell type class for automatic 'HOrd' inference.
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


-- TODO: class HPER (a :: Hakaru)
-- TODO: class HPartialOrder (a :: Hakaru)

----------------------------------------------------------------
-- | Concrete dictionaries for Hakaru types which are semirings.
-- N.B., even though these particular semirings are commutative,
-- we don't necessarily assume that.
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 -- This one could be derived...
    == :: 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

-- BUG: deriving instance Read (HSemiring a)
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

-- | Haskell type class for automatic 'HSemiring' inference.
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 


----------------------------------------------------------------
-- | Concrete dictionaries for Hakaru types which are rings. N.B.,
-- even though these particular rings are commutative, we don't
-- necessarily assume that.
data HRing :: Hakaru -> * where
    HRing_Int  :: HRing 'HInt
    HRing_Real :: HRing 'HReal


instance Eq (HRing a) where -- This one could be derived...
    == :: 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

    
-- BUG: deriving instance Read (HRing a)

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

-- hNonNegative_Sing :: Sing (NonNegative a) -> Maybe (HRing a)

-- | Every 'HRing' is a 'HSemiring'.
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

-- | The non-negative type of every 'HRing' is a 'HSemiring'.
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

-- | 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?
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



----------------------------------------------------------------
-- N.B., We're assuming two-sided inverses here. That doesn't entail
-- commutativity, though it does strongly suggest it... (cf.,
-- Wedderburn's little theorem)
--
-- N.B., the (Nat,"+"=lcm,"*"=gcd) semiring is sometimes called
-- "the division semiring"
--
-- HACK: tracking the generating carriers here wouldn't be quite
-- right b/c we get more than just the (non-negative)rationals
-- generated from HNat/HInt! However, we should have some sort of
-- associated type so we can add rationals and non-negative
-- rationals...
--
-- TODO: associated type for non-zero elements. To guarantee the
-- safety of division\/recip? For now, we have Infinity, so it's
-- actually safe for these two types. But if we want to add the
-- rationals...
--
-- | 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.
data HFractional :: Hakaru -> * where
    HFractional_Prob :: HFractional 'HProb
    HFractional_Real :: HFractional 'HReal


instance Eq (HFractional a) where -- This one could be derived...
    == :: 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

-- BUG: deriving instance Read (HFractional a)
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

-- | Every 'HFractional' is a 'HSemiring'.
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

-- | Haskell type class for automatic 'HFractional' inference.
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 


-- type HDivisionRing a = (HFractional a, HRing a)
-- type HField a = (HDivisionRing a, HCommutativeSemiring a)


----------------------------------------------------------------
-- Numbers formed by finitely many uses of integer addition,
-- subtraction, multiplication, division, and nat-roots are all
-- algebraic; however, N.B., not all algebraic numbers can be formed
-- this way (cf., Abel–Ruffini theorem)
-- TODO: ought we require HFractional rather than HSemiring?
-- TODO: any special associated type?
--
-- | 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.
data HRadical :: Hakaru -> * where
    HRadical_Prob :: HRadical 'HProb


instance Eq (HRadical a) where -- This one could be derived...
    == :: 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

-- BUG: deriving instance Read (HRadical a)
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

-- | Every 'HRadical' is a 'HSemiring'.
hSemiring_HRadical :: HRadical a -> HSemiring a
hSemiring_HRadical :: HRadical a -> HSemiring a
hSemiring_HRadical HRadical a
HRadical_Prob = HSemiring a
HSemiring 'HProb
HSemiring_Prob

-- | Haskell type class for automatic 'HRadical' inference.
class (HSemiring_ a) => HRadical_ (a :: Hakaru) where
    hRadical :: HRadical a
instance HRadical_ 'HProb where hRadical :: HRadical 'HProb
hRadical = HRadical 'HProb
HRadical_Prob 


-- TODO: class (HDivisionRing a, HRadical a) => HAlgebraic a where...

-- | Concrete dictionaries for types where Infinity can have
data HIntegrable :: Hakaru -> * where
    HIntegrable_Nat  :: HIntegrable 'HNat
    HIntegrable_Prob :: HIntegrable 'HProb

instance Eq (HIntegrable a) where -- This one could be derived...
    == :: 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

-- BUG: deriving instance Read (HIntegrable a)
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

-- | Concrete dictionaries for Hakaru types which are \"discrete\".
data HDiscrete :: Hakaru -> * where
    HDiscrete_Nat :: HDiscrete 'HNat
    HDiscrete_Int :: HDiscrete 'HInt

instance Eq (HDiscrete a) where -- This one could be derived...
    == :: 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

-- BUG: deriving instance Read (HDiscrete a)
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

-- | Haskell type class for automatic 'HDiscrete' inference.
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 

----------------------------------------------------------------
-- TODO: find better names than HContinuous and HIntegral
-- TODO: how to require that "if HRing a, then HRing b too"?
-- TODO: should we call this something like Dedekind-complete?
-- That's what distinguishes the reals from the rationals. Of course,
-- calling it that suggests (but does not require) that we should
-- have some supremum operator; but supremum only differs from
-- maximum if we have some way of talking about infinite sets of
-- values (which is surely too much to bother with).
--
-- | 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@.
data HContinuous :: Hakaru -> * where
    HContinuous_Prob :: HContinuous 'HProb
    HContinuous_Real :: HContinuous 'HReal


instance Eq (HContinuous a) where -- This one could be derived...
    == :: 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

-- BUG: deriving instance Read (HContinuous a)
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

-- hIntegral_Sing :: Sing (HIntegral a) -> Maybe (HContinuous a)

-- | Every 'HContinuous' is a 'HFractional'.
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

-- | The integral type of every 'HContinuous' is a 'HSemiring'.
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

-- | 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?
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


----------------------------------------------------------------
----------------------------------------------------------- fin.