{-# 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 ---------------------------------------------------------------- -- | 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_Nat = SNat sing_HEq HEq_Int = SInt sing_HEq HEq_Prob = SProb sing_HEq HEq_Real = SReal sing_HEq (HEq_Array a) = SArray (sing_HEq a) sing_HEq HEq_Bool = sBool sing_HEq HEq_Unit = sUnit sing_HEq (HEq_Pair a b) = sPair (sing_HEq a) (sing_HEq b) sing_HEq (HEq_Either a b) = sEither (sing_HEq a) (sing_HEq b) hEq_Sing :: Sing a -> Maybe (HEq a) hEq_Sing SNat = Just HEq_Nat hEq_Sing SInt = Just HEq_Int hEq_Sing SProb = Just HEq_Prob hEq_Sing SReal = Just HEq_Real hEq_Sing (SArray a) = HEq_Array <$> hEq_Sing a hEq_Sing s = (jmEq1 s sUnit >>= \Refl -> Just HEq_Unit) <|> (jmEq1 s sBool >>= \Refl -> Just HEq_Bool) {- hEq_Sing (sPair a b) = HEq_Pair <$> hEq_Sing a <*> hEq_Sing b hEq_Sing (sEither a b) = HEq_Either <$> hEq_Sing a <*> hEq_Sing b -} -- | Haskell type class for automatic 'HEq' inference. class HEq_ (a :: Hakaru) where hEq :: HEq a instance HEq_ 'HNat where hEq = HEq_Nat instance HEq_ 'HInt where hEq = HEq_Int instance HEq_ 'HProb where hEq = HEq_Prob instance HEq_ 'HReal where hEq = HEq_Real instance HEq_ HBool where hEq = HEq_Bool instance HEq_ HUnit where hEq = HEq_Unit instance (HEq_ a) => HEq_ ('HArray a) where hEq = HEq_Array hEq instance (HEq_ a, HEq_ b) => HEq_ (HPair a b) where hEq = HEq_Pair hEq hEq instance (HEq_ a, HEq_ b) => HEq_ (HEither a b) where hEq = HEq_Either hEq 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_Nat = SNat sing_HOrd HOrd_Int = SInt sing_HOrd HOrd_Prob = SProb sing_HOrd HOrd_Real = SReal sing_HOrd (HOrd_Array a) = SArray (sing_HOrd a) sing_HOrd HOrd_Bool = sBool sing_HOrd HOrd_Unit = sUnit sing_HOrd (HOrd_Pair a b) = sPair (sing_HOrd a) (sing_HOrd b) sing_HOrd (HOrd_Either a b) = sEither (sing_HOrd a) (sing_HOrd b) hOrd_Sing :: Sing a -> Maybe (HOrd a) hOrd_Sing SNat = Just HOrd_Nat hOrd_Sing SInt = Just HOrd_Int hOrd_Sing SProb = Just HOrd_Prob hOrd_Sing SReal = Just HOrd_Real hOrd_Sing (SArray a) = HOrd_Array <$> hOrd_Sing a hOrd_Sing _ = Nothing -- | Every 'HOrd' type is 'HEq'. hEq_HOrd :: HOrd a -> HEq a hEq_HOrd HOrd_Nat = HEq_Nat hEq_HOrd HOrd_Int = HEq_Int hEq_HOrd HOrd_Prob = HEq_Prob hEq_HOrd HOrd_Real = HEq_Real hEq_HOrd (HOrd_Array a) = HEq_Array (hEq_HOrd a) hEq_HOrd HOrd_Bool = HEq_Bool hEq_HOrd HOrd_Unit = HEq_Unit hEq_HOrd (HOrd_Pair a b) = HEq_Pair (hEq_HOrd a) (hEq_HOrd b) hEq_HOrd (HOrd_Either a b) = HEq_Either (hEq_HOrd a) (hEq_HOrd b) -- | Haskell type class for automatic 'HOrd' inference. class HEq_ a => HOrd_ (a :: Hakaru) where hOrd :: HOrd a instance HOrd_ 'HNat where hOrd = HOrd_Nat instance HOrd_ 'HInt where hOrd = HOrd_Int instance HOrd_ 'HProb where hOrd = HOrd_Prob instance HOrd_ 'HReal where hOrd = HOrd_Real instance HOrd_ HBool where hOrd = HOrd_Bool instance HOrd_ HUnit where hOrd = HOrd_Unit instance (HOrd_ a) => HOrd_ ('HArray a) where hOrd = HOrd_Array hOrd instance (HOrd_ a, HOrd_ b) => HOrd_ (HPair a b) where hOrd = HOrd_Pair hOrd hOrd instance (HOrd_ a, HOrd_ b) => HOrd_ (HEither a b) where hOrd = HOrd_Either hOrd 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... (==) = eq1 instance Eq1 HSemiring where eq1 x y = maybe False (const True) (jmEq1 x y) instance JmEq1 HSemiring where jmEq1 HSemiring_Nat HSemiring_Nat = Just Refl jmEq1 HSemiring_Int HSemiring_Int = Just Refl jmEq1 HSemiring_Prob HSemiring_Prob = Just Refl jmEq1 HSemiring_Real HSemiring_Real = Just Refl jmEq1 _ _ = Nothing -- BUG: deriving instance Read (HSemiring a) deriving instance Show (HSemiring a) sing_HSemiring :: HSemiring a -> Sing a sing_HSemiring HSemiring_Nat = SNat sing_HSemiring HSemiring_Int = SInt sing_HSemiring HSemiring_Prob = SProb sing_HSemiring HSemiring_Real = SReal hSemiring_Sing :: Sing a -> Maybe (HSemiring a) hSemiring_Sing SNat = Just HSemiring_Nat hSemiring_Sing SInt = Just HSemiring_Int hSemiring_Sing SProb = Just HSemiring_Prob hSemiring_Sing SReal = Just HSemiring_Real hSemiring_Sing _ = Nothing -- | Haskell type class for automatic 'HSemiring' inference. class HSemiring_ (a :: Hakaru) where hSemiring :: HSemiring a instance HSemiring_ 'HNat where hSemiring = HSemiring_Nat instance HSemiring_ 'HInt where hSemiring = HSemiring_Int instance HSemiring_ 'HProb where hSemiring = HSemiring_Prob instance HSemiring_ 'HReal where hSemiring = 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... (==) = eq1 instance Eq1 HRing where eq1 x y = maybe False (const True) (jmEq1 x y) instance JmEq1 HRing where jmEq1 HRing_Int HRing_Int = Just Refl jmEq1 HRing_Real HRing_Real = Just Refl jmEq1 _ _ = Nothing -- BUG: deriving instance Read (HRing a) deriving instance Show (HRing a) sing_HRing :: HRing a -> Sing a sing_HRing HRing_Int = SInt sing_HRing HRing_Real = SReal hRing_Sing :: Sing a -> Maybe (HRing a) hRing_Sing SInt = Just HRing_Int hRing_Sing SReal = Just HRing_Real hRing_Sing _ = Nothing sing_NonNegative :: HRing a -> Sing (NonNegative a) sing_NonNegative = sing_HSemiring . hSemiring_NonNegativeHRing -- hNonNegative_Sing :: Sing (NonNegative a) -> Maybe (HRing a) -- | Every 'HRing' is a 'HSemiring'. hSemiring_HRing :: HRing a -> HSemiring a hSemiring_HRing HRing_Int = HSemiring_Int hSemiring_HRing HRing_Real = HSemiring_Real -- | The non-negative type of every 'HRing' is a 'HSemiring'. hSemiring_NonNegativeHRing :: HRing a -> HSemiring (NonNegative a) hSemiring_NonNegativeHRing HRing_Int = HSemiring_Nat hSemiring_NonNegativeHRing HRing_Real = 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_Int instance HRing_ 'HReal where type NonNegative 'HReal = 'HProb hRing = 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... (==) = eq1 instance Eq1 HFractional where eq1 x y = maybe False (const True) (jmEq1 x y) instance JmEq1 HFractional where jmEq1 HFractional_Prob HFractional_Prob = Just Refl jmEq1 HFractional_Real HFractional_Real = Just Refl jmEq1 _ _ = Nothing -- BUG: deriving instance Read (HFractional a) deriving instance Show (HFractional a) sing_HFractional :: HFractional a -> Sing a sing_HFractional HFractional_Prob = SProb sing_HFractional HFractional_Real = SReal hFractional_Sing :: Sing a -> Maybe (HFractional a) hFractional_Sing SProb = Just HFractional_Prob hFractional_Sing SReal = Just HFractional_Real hFractional_Sing _ = Nothing -- | Every 'HFractional' is a 'HSemiring'. hSemiring_HFractional :: HFractional a -> HSemiring a hSemiring_HFractional HFractional_Prob = HSemiring_Prob hSemiring_HFractional HFractional_Real = 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_Prob instance HFractional_ 'HReal where hFractional = 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... (==) = eq1 instance Eq1 HRadical where eq1 x y = maybe False (const True) (jmEq1 x y) instance JmEq1 HRadical where jmEq1 HRadical_Prob HRadical_Prob = Just Refl -- BUG: deriving instance Read (HRadical a) deriving instance Show (HRadical a) sing_HRadical :: HRadical a -> Sing a sing_HRadical HRadical_Prob = SProb hRadical_Sing :: Sing a -> Maybe (HRadical a) hRadical_Sing SProb = Just HRadical_Prob hRadical_Sing _ = Nothing -- | Every 'HRadical' is a 'HSemiring'. hSemiring_HRadical :: HRadical a -> HSemiring a hSemiring_HRadical HRadical_Prob = 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_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... (==) = eq1 instance Eq1 HIntegrable where eq1 x y = maybe False (const True) (jmEq1 x y) instance JmEq1 HIntegrable where jmEq1 HIntegrable_Nat HIntegrable_Nat = Just Refl jmEq1 HIntegrable_Prob HIntegrable_Prob = Just Refl jmEq1 _ _ = Nothing -- BUG: deriving instance Read (HIntegrable a) deriving instance Show (HIntegrable a) sing_HIntegrable :: HIntegrable a -> Sing a sing_HIntegrable HIntegrable_Nat = SNat sing_HIntegrable HIntegrable_Prob = SProb hIntegrable_Sing :: Sing a -> Maybe (HIntegrable a) hIntegrable_Sing SNat = Just HIntegrable_Nat hIntegrable_Sing SProb = Just HIntegrable_Prob hIntegrable_Sing _ = 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... (==) = eq1 instance Eq1 HDiscrete where eq1 x y = maybe False (const True) (jmEq1 x y) instance JmEq1 HDiscrete where jmEq1 HDiscrete_Nat HDiscrete_Nat = Just Refl jmEq1 HDiscrete_Int HDiscrete_Int = Just Refl jmEq1 _ _ = Nothing -- BUG: deriving instance Read (HDiscrete a) deriving instance Show (HDiscrete a) sing_HDiscrete :: HDiscrete a -> Sing a sing_HDiscrete HDiscrete_Nat = SNat sing_HDiscrete HDiscrete_Int = SInt hDiscrete_Sing :: Sing a -> Maybe (HDiscrete a) hDiscrete_Sing SNat = Just HDiscrete_Nat hDiscrete_Sing SInt = Just HDiscrete_Int hDiscrete_Sing _ = Nothing -- | Haskell type class for automatic 'HDiscrete' inference. class (HSemiring_ a) => HDiscrete_ (a :: Hakaru) where hDiscrete :: HDiscrete a instance HDiscrete_ 'HNat where hDiscrete = HDiscrete_Nat instance HDiscrete_ 'HInt where hDiscrete = 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... (==) = eq1 instance Eq1 HContinuous where eq1 x y = maybe False (const True) (jmEq1 x y) instance JmEq1 HContinuous where jmEq1 HContinuous_Prob HContinuous_Prob = Just Refl jmEq1 HContinuous_Real HContinuous_Real = Just Refl jmEq1 _ _ = Nothing -- BUG: deriving instance Read (HContinuous a) deriving instance Show (HContinuous a) sing_HContinuous :: HContinuous a -> Sing a sing_HContinuous HContinuous_Prob = SProb sing_HContinuous HContinuous_Real = SReal hContinuous_Sing :: Sing a -> Maybe (HContinuous a) hContinuous_Sing SProb = Just HContinuous_Prob hContinuous_Sing SReal = Just HContinuous_Real hContinuous_Sing _ = Nothing sing_HIntegral :: HContinuous a -> Sing (HIntegral a) sing_HIntegral = sing_HSemiring . hSemiring_HIntegralContinuous -- hIntegral_Sing :: Sing (HIntegral a) -> Maybe (HContinuous a) -- | Every 'HContinuous' is a 'HFractional'. hFractional_HContinuous :: HContinuous a -> HFractional a hFractional_HContinuous HContinuous_Prob = HFractional_Prob hFractional_HContinuous HContinuous_Real = HFractional_Real -- | The integral type of every 'HContinuous' is a 'HSemiring'. hSemiring_HIntegralContinuous :: HContinuous a -> HSemiring (HIntegral a) hSemiring_HIntegralContinuous HContinuous_Prob = HSemiring_Nat hSemiring_HIntegralContinuous HContinuous_Real = 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_Prob instance HContinuous_ 'HReal where type HIntegral 'HReal = 'HInt hContinuous = HContinuous_Real ---------------------------------------------------------------- ----------------------------------------------------------- fin.