{-# LANGUAGE CPP
           , DataKinds
           , PolyKinds
           , GADTs
           , StandaloneDeriving
           , TypeOperators
           , TypeFamilies
           , FlexibleContexts
           , UndecidableInstances
           , Rank2Types
           , DeriveDataTypeable
           , LambdaCase
           #-}

{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
----------------------------------------------------------------
--                                                    2016.02.21
-- |
-- Module      :  Language.Hakaru.Syntax.AST
-- Copyright   :  Copyright (c) 2016 the Hakaru team
-- License     :  BSD3
-- Maintainer  :  wren@community.haskell.org
-- Stability   :  experimental
-- Portability :  GHC-only
--
-- The generating functor for the raw syntax, along with various
-- helper types. For a more tutorial sort of introduction to how
-- things are structured here and in "Language.Hakaru.Syntax.ABT",
-- see <http://winterkoninkje.dreamwidth.org/103978.html>
--
-- TODO: are we finally at the place where we can get rid of all
-- those annoying underscores?
--
-- TODO: what is the runtime cost of storing all these dictionary
-- singletons? For existential type variables, it should be the
-- same as using a type class constraint; but for non-existential
-- type variables it'll, what, double the size of the AST?
----------------------------------------------------------------
module Language.Hakaru.Syntax.AST
    (
    -- * Syntactic forms
      SCon(..)
    , SArgs(..)
    , Term(..)
    , Transform(..), TransformImpl(..)
    -- allTransforms, transformName comes from Transform
    -- * Operators
    , LCs, UnLCs -- LC comes from SArgs
    , LC_(..)
    , NaryOp(..)
    , PrimOp(..)
    , ArrayOp(..)
    , MeasureOp(..)
    -- * Constant values
    , Literal(..)
    
    -- * implementation details
    , foldMapPairs
    , traversePairs
    , module Language.Hakaru.Syntax.SArgs
    , module Language.Hakaru.Syntax.Transform
    ) where

import           Data.Sequence (Seq)
import qualified Data.Foldable as F
import qualified Data.List.NonEmpty as L
#if __GLASGOW_HASKELL__ < 710
import           Data.Monoid   (Monoid(..))
import           Control.Applicative
import           Data.Traversable
#endif

import           Control.Arrow ((***))
import           Data.Ratio    (numerator, denominator)

import Data.Data ()

import Data.Number.Natural
import Language.Hakaru.Syntax.IClasses
import Language.Hakaru.Types.DataKind
import Language.Hakaru.Types.Sing
import Language.Hakaru.Types.HClasses
import Language.Hakaru.Types.Coercion
import Language.Hakaru.Syntax.Datum
import Language.Hakaru.Syntax.Reducer
import Language.Hakaru.Syntax.ABT (ABT(syn))

import Language.Hakaru.Syntax.SArgs
import Language.Hakaru.Syntax.Transform

----------------------------------------------------------------
----------------------------------------------------------------
-- BUG: can't UNPACK 'Integer' and 'Natural' like we can for 'Int' and 'Nat'
--
-- | Numeric literals for the primitive numeric types. In addition
-- to being normal forms, these are also ground terms: that is, not
-- only are they closed (i.e., no free variables), they also have
-- no bound variables and thus no binding forms. Notably, we store
-- literals using exact types so that none of our program transformations
-- have to worry about issues like overflow or floating-point fuzz.
data Literal :: Hakaru -> * where
    LNat   :: !Natural -> Literal 'HNat
    LInt   :: !Integer -> Literal 'HInt
    LProb  :: {-# UNPACK #-} !NonNegativeRational -> Literal 'HProb
    LReal  :: {-# UNPACK #-} !Rational            -> Literal 'HReal

instance JmEq1 Literal where
    jmEq1 :: Literal i -> Literal j -> Maybe (TypeEq i j)
jmEq1 (LNat  Natural
x) (LNat  Natural
y) = if Natural
x Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
y then TypeEq i i -> Maybe (TypeEq i i)
forall a. a -> Maybe a
Just TypeEq i i
forall k (a :: k). TypeEq a a
Refl else Maybe (TypeEq i j)
forall a. Maybe a
Nothing
    jmEq1 (LInt  Integer
x) (LInt  Integer
y) = if Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
y then TypeEq i i -> Maybe (TypeEq i i)
forall a. a -> Maybe a
Just TypeEq i i
forall k (a :: k). TypeEq a a
Refl else Maybe (TypeEq i j)
forall a. Maybe a
Nothing
    jmEq1 (LProb NonNegativeRational
x) (LProb NonNegativeRational
y) = if NonNegativeRational
x NonNegativeRational -> NonNegativeRational -> Bool
forall a. Eq a => a -> a -> Bool
== NonNegativeRational
y then TypeEq i i -> Maybe (TypeEq i i)
forall a. a -> Maybe a
Just TypeEq i i
forall k (a :: k). TypeEq a a
Refl else Maybe (TypeEq i j)
forall a. Maybe a
Nothing
    jmEq1 (LReal Rational
x) (LReal Rational
y) = if Rational
x Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Rational
y then TypeEq i i -> Maybe (TypeEq i i)
forall a. a -> Maybe a
Just TypeEq i i
forall k (a :: k). TypeEq a a
Refl else Maybe (TypeEq i j)
forall a. Maybe a
Nothing
    jmEq1 Literal i
_         Literal j
_         = Maybe (TypeEq i j)
forall a. Maybe a
Nothing

instance Eq1 Literal where
    eq1 :: Literal i -> Literal i -> Bool
eq1 (LNat  Natural
x) (LNat  Natural
y) = Natural
x Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
y
    eq1 (LInt  Integer
x) (LInt  Integer
y) = Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
y
    eq1 (LProb NonNegativeRational
x) (LProb NonNegativeRational
y) = NonNegativeRational
x NonNegativeRational -> NonNegativeRational -> Bool
forall a. Eq a => a -> a -> Bool
== NonNegativeRational
y
    eq1 (LReal Rational
x) (LReal Rational
y) = Rational
x Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Rational
y
    -- Because of GADTs, the following is apparently redundant
    -- eq1 _         _          = False

instance Eq (Literal a) where
    == :: Literal a -> Literal a -> Bool
(==) = Literal a -> Literal a -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1

-- TODO: instance Read (Literal a)

instance Show1 Literal where
    showsPrec1 :: Int -> Literal i -> ShowS
showsPrec1 Int
p Literal i
t =
        case Literal i
t of
        LNat  Natural
v -> Int -> String -> Natural -> ShowS
forall a. Show a => Int -> String -> a -> ShowS
showParen_0 Int
p String
"LNat"  Natural
v
        LInt  Integer
v -> Int -> String -> Integer -> ShowS
forall a. Show a => Int -> String -> a -> ShowS
showParen_0 Int
p String
"LInt"  Integer
v
        LProb NonNegativeRational
v -> Int -> String -> NonNegativeRational -> ShowS
forall a. Show a => Int -> String -> a -> ShowS
showParen_0 Int
p String
"LProb" NonNegativeRational
v -- TODO: pretty print as decimals instead of using the Show Rational instance
        LReal Rational
v -> Int -> String -> Rational -> ShowS
forall a. Show a => Int -> String -> a -> ShowS
showParen_0 Int
p String
"LReal" Rational
v -- TODO: pretty print as decimals instead of using the Show Rational instance

instance Show (Literal a) where
    showsPrec :: Int -> Literal a -> ShowS
showsPrec = Int -> Literal a -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1
    show :: Literal a -> String
show      = Literal a -> String
forall k (a :: k -> *) (i :: k). Show1 a => a i -> String
show1


-- TODO: first optimize the @Coercion a b@ to choose the most desirable of many equivalent paths?
instance Coerce Literal where
    coerceTo :: Coercion a b -> Literal a -> Literal b
coerceTo   Coercion a b
CNil         Literal a
v = Literal a
Literal b
v
    coerceTo   (CCons PrimCoercion a b
c Coercion b b
cs) Literal a
v = Coercion b b -> Literal b -> Literal b
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
Coerce f =>
Coercion a b -> f a -> f b
coerceTo Coercion b b
cs (PrimCoercion a b -> Literal a -> Literal b
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
PrimCoerce f =>
PrimCoercion a b -> f a -> f b
primCoerceTo PrimCoercion a b
c Literal a
v)

    coerceFrom :: Coercion a b -> Literal b -> Literal a
coerceFrom Coercion a b
CNil         Literal b
v = Literal a
Literal b
v
    coerceFrom (CCons PrimCoercion a b
c Coercion b b
cs) Literal b
v = PrimCoercion a b -> Literal b -> Literal a
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
PrimCoerce f =>
PrimCoercion a b -> f b -> f a
primCoerceFrom PrimCoercion a b
c (Coercion b b -> Literal b -> Literal b
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
Coerce f =>
Coercion a b -> f b -> f a
coerceFrom Coercion b b
cs Literal b
v)

instance PrimCoerce Literal where
    primCoerceTo :: PrimCoercion a b -> Literal a -> Literal b
primCoerceTo PrimCoercion a b
c =
        case PrimCoercion a b
c of
        Signed     HRing b
HRing_Int        -> \(LNat  Natural
n) -> Integer -> Literal 'HInt
LInt  (Natural -> Integer
nat2int   Natural
n)
        Signed     HRing b
HRing_Real       -> \(LProb NonNegativeRational
p) -> Rational -> Literal 'HReal
LReal (NonNegativeRational -> Rational
prob2real NonNegativeRational
p)
        Continuous HContinuous b
HContinuous_Prob -> \(LNat  Natural
n) -> NonNegativeRational -> Literal 'HProb
LProb (Natural -> NonNegativeRational
nat2prob  Natural
n)
        Continuous HContinuous b
HContinuous_Real -> \(LInt  Integer
i) -> Rational -> Literal 'HReal
LReal (Integer -> Rational
int2real  Integer
i)
        where
        -- HACK: type signatures needed to avoid defaulting
        nat2int   :: Natural -> Integer
        nat2int :: Natural -> Integer
nat2int   = Natural -> Integer
fromNatural
        nat2prob  :: Natural -> NonNegativeRational
        nat2prob :: Natural -> NonNegativeRational
nat2prob  = Rational -> NonNegativeRational
unsafeNonNegativeRational (Rational -> NonNegativeRational)
-> (Natural -> Rational) -> Natural -> NonNegativeRational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> Rational
forall a. Real a => a -> Rational
toRational -- N.B., is actually safe here
        prob2real :: NonNegativeRational -> Rational
        prob2real :: NonNegativeRational -> Rational
prob2real = NonNegativeRational -> Rational
fromNonNegativeRational
        int2real  :: Integer -> Rational
        int2real :: Integer -> Rational
int2real  = Integer -> Rational
forall a b. (Integral a, Num b) => a -> b
fromIntegral

    primCoerceFrom :: PrimCoercion a b -> Literal b -> Literal a
primCoerceFrom PrimCoercion a b
c =
        case PrimCoercion a b
c of
        Signed     HRing b
HRing_Int        -> \(LInt  Integer
i) -> Natural -> Literal 'HNat
LNat  (Integer -> Natural
int2nat   Integer
i)
        Signed     HRing b
HRing_Real       -> \(LReal Rational
r) -> NonNegativeRational -> Literal 'HProb
LProb (Rational -> NonNegativeRational
real2prob Rational
r)
        Continuous HContinuous b
HContinuous_Prob -> \(LProb NonNegativeRational
p) -> Natural -> Literal 'HNat
LNat  (NonNegativeRational -> Natural
prob2nat  NonNegativeRational
p)
        Continuous HContinuous b
HContinuous_Real -> \(LReal Rational
r) -> Integer -> Literal 'HInt
LInt  (Rational -> Integer
real2int  Rational
r)
        where
        -- HACK: type signatures needed to avoid defaulting
        -- TODO: how to handle the errors? Generate error code in hakaru? capture it in a monad?
        int2nat  :: Integer -> Natural
        int2nat :: Integer -> Natural
int2nat Integer
x =
            case Integer -> Maybe Natural
toNatural Integer
x of
            Just Natural
y  -> Natural
y
            Maybe Natural
Nothing -> String -> Natural
forall a. HasCallStack => String -> a
error (String -> Natural) -> String -> Natural
forall a b. (a -> b) -> a -> b
$ String
"primCoerceFrom@Literal: negative HInt " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
x
        prob2nat :: NonNegativeRational -> Natural
        prob2nat :: NonNegativeRational -> Natural
prob2nat NonNegativeRational
x =
            if NonNegativeRational -> Natural
forall a. Ratio a -> a
denominator NonNegativeRational
x Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
1
            then NonNegativeRational -> Natural
forall a. Ratio a -> a
numerator NonNegativeRational
x
            else String -> Natural
forall a. HasCallStack => String -> a
error (String -> Natural) -> String -> Natural
forall a b. (a -> b) -> a -> b
$ String
"primCoerceFrom@Literal: non-integral HProb " String -> ShowS
forall a. [a] -> [a] -> [a]
++ NonNegativeRational -> String
forall a. Show a => a -> String
show NonNegativeRational
x
        real2prob :: Rational -> NonNegativeRational
        real2prob :: Rational -> NonNegativeRational
real2prob Rational
x =
            case Rational -> Maybe NonNegativeRational
toNonNegativeRational Rational
x of
            Just NonNegativeRational
y  -> NonNegativeRational
y
            Maybe NonNegativeRational
Nothing -> String -> NonNegativeRational
forall a. HasCallStack => String -> a
error (String -> NonNegativeRational) -> String -> NonNegativeRational
forall a b. (a -> b) -> a -> b
$ String
"primCoerceFrom@Literal: negative HReal " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Rational -> String
forall a. Show a => a -> String
show Rational
x
        real2int :: Rational -> Integer
        real2int :: Rational -> Integer
real2int Rational
x =
            if Rational -> Integer
forall a. Ratio a -> a
denominator Rational
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1
            then Rational -> Integer
forall a. Ratio a -> a
numerator Rational
x
            else String -> Integer
forall a. HasCallStack => String -> a
error (String -> Integer) -> String -> Integer
forall a b. (a -> b) -> a -> b
$ String
"primCoerceFrom@Literal: non-integral HReal " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Rational -> String
forall a. Show a => a -> String
show Rational
x


----------------------------------------------------------------
-- TODO: helper functions for splitting NaryOp_ into components to group up like things. (e.g., grouping all the Literals together so we can do constant propagation)

-- | Primitive associative n-ary functions. By flattening the trees
-- for associative operators, we can more easily perform equivalence
-- checking and pattern matching (e.g., to convert @exp (a * log
-- b)@ into @b ** a@, regardless of whether @a@ is a product of
-- things or not). Notably, because of this encoding, we encode
-- things like subtraction and division by their unary operators
-- (negation and reciprocal).
--
-- We do not make any assumptions about whether these semigroups
-- are monoids, commutative, idempotent, or anything else. That has
-- to be handled by transformations, rather than by the AST itself.
data NaryOp :: Hakaru -> * where
    And  :: NaryOp HBool
    Or   :: NaryOp HBool
    Xor  :: NaryOp HBool
    -- N.B., even though 'Iff' is associative (in Boolean algebras),
    -- we should not support n-ary uses in our *surface* syntax.
    -- Because it's too easy for folks to confuse "a <=> b <=> c"
    -- with "(a <=> b) /\ (b <=> c)".
    Iff  :: NaryOp HBool -- == Not (Xor x y)

    -- These two don't necessarily have identity elements; thus,
    -- @NaryOp_ Min []@ and @NaryOp_ Max []@ may not be well-defined...
    -- TODO: check for those cases!
    Min  :: !(HOrd a) -> NaryOp a
    Max  :: !(HOrd a) -> NaryOp a

    Sum  :: !(HSemiring a) -> NaryOp a
    Prod :: !(HSemiring a) -> NaryOp a

    {-
    GCD  :: !(GCD_Domain a) -> NaryOp a
    LCM  :: !(GCD_Domain a) -> NaryOp a
    -}

-- TODO: instance Read (NaryOp a)
deriving instance Show (NaryOp a)

instance JmEq1 NaryOp where
    jmEq1 :: NaryOp i -> NaryOp j -> Maybe (TypeEq i j)
jmEq1 NaryOp i
And      NaryOp j
And      = 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 NaryOp i
Or       NaryOp j
Or       = 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 NaryOp i
Xor      NaryOp j
Xor      = 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 NaryOp i
Iff      NaryOp j
Iff      = 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 (Min  HOrd i
a) (Min  HOrd j
b) = Sing i -> Sing j -> Maybe (TypeEq i j)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 (HOrd i -> Sing i
forall (a :: Hakaru). HOrd a -> Sing a
sing_HOrd HOrd i
a) (HOrd j -> Sing j
forall (a :: Hakaru). HOrd a -> Sing a
sing_HOrd HOrd j
b)
    jmEq1 (Max  HOrd i
a) (Max  HOrd j
b) = Sing i -> Sing j -> Maybe (TypeEq i j)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 (HOrd i -> Sing i
forall (a :: Hakaru). HOrd a -> Sing a
sing_HOrd HOrd i
a) (HOrd j -> Sing j
forall (a :: Hakaru). HOrd a -> Sing a
sing_HOrd HOrd j
b)
    jmEq1 (Sum  HSemiring i
a) (Sum  HSemiring j
b) = HSemiring i -> HSemiring j -> Maybe (TypeEq i j)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 HSemiring i
a HSemiring j
b
    jmEq1 (Prod HSemiring i
a) (Prod HSemiring j
b) = HSemiring i -> HSemiring j -> Maybe (TypeEq i j)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 HSemiring i
a HSemiring j
b
    jmEq1 NaryOp i
_        NaryOp j
_        = Maybe (TypeEq i j)
forall a. Maybe a
Nothing

-- TODO: We could optimize this like we do for 'Literal'
instance Eq1 NaryOp where
    eq1 :: NaryOp i -> NaryOp i -> Bool
eq1 NaryOp i
x NaryOp 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) (NaryOp i -> NaryOp i -> Maybe (TypeEq i i)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 NaryOp i
x NaryOp i
y)

instance Eq (NaryOp a) where -- This one can be derived
    == :: NaryOp a -> NaryOp a -> Bool
(==) = NaryOp a -> NaryOp a -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1


----------------------------------------------------------------
-- TODO: should we define our own datakind for @([Hakaru], Hakaru)@ or perhaps for the @/\a -> ([a], Hakaru)@ part of it?

-- BUG: how to declare that these are inverses?
type family LCs (xs :: [Hakaru]) :: [([Hakaru], Hakaru)] where
    LCs '[]       = '[]
    LCs (x ': xs) = LC x ': LCs xs

type family UnLCs (xs :: [([Hakaru], Hakaru)]) :: [Hakaru] where
    UnLCs '[]                  = '[]
    UnLCs ( '( '[], x ) ': xs) = x ': UnLCs xs


-- | Simple primitive functions, and constants. N.B., nothing in
-- here should produce or consume things of 'HMeasure' or 'HArray'
-- type (except perhaps in a totally polymorphic way).
data PrimOp :: [Hakaru] -> Hakaru -> * where

    -- -- -- Here we have /monomorphic/ operators
    -- -- The Boolean operators
    -- TODO: most of these we'll want to optimize away according
    -- to some circuit-minimization procedure. But we're not
    -- committing to any particular minimal complete set of primops
    -- just yet.
    -- N.B., general circuit minimization problem is Sigma_2^P-complete,
    -- which is outside of PTIME; so we'll just have to approximate
    -- it for now, or link into something like Espresso or an
    -- implementation of Quine–McCluskey
    -- cf., <https://hackage.haskell.org/package/qm-0.1.0.0/candidate>
    -- cf., <https://github.com/pfpacket/Quine-McCluskey>
    -- cf., <https://gist.github.com/dsvictor94/8db2b399a95e301c259a>
    Not  :: PrimOp '[ HBool ] HBool
    -- And, Or, Xor, Iff
    Impl :: PrimOp '[ HBool, HBool ] HBool
    -- Impl x y == Or (Not x) y
    Diff :: PrimOp '[ HBool, HBool ] HBool
    -- Diff x y == Not (Impl x y)
    Nand :: PrimOp '[ HBool, HBool ] HBool
    -- Nand aka Alternative Denial, Sheffer stroke
    Nor  :: PrimOp '[ HBool, HBool ] HBool
    -- Nor aka Joint Denial, aka Quine dagger, aka Pierce arrow
    --
    -- The remaining eight binops are completely uninteresting:
    --   flip Impl
    --   flip Diff
    --   const
    --   flip const
    --   (Not .) . const == const . Not
    --   (Not .) . flip const
    --   const (const True)
    --   const (const False)


    -- -- Trigonometry operators
    Pi    :: PrimOp '[] 'HProb -- TODO: maybe make this HContinuous polymorphic?
    -- TODO: if we're going to bother naming the hyperbolic ones, why not also name /a?(csc|sec|cot)h?/ eh?
    -- TODO: capture more domain information in these types?
    Sin   :: PrimOp '[ 'HReal ] 'HReal
    Cos   :: PrimOp '[ 'HReal ] 'HReal
    Tan   :: PrimOp '[ 'HReal ] 'HReal
    Asin  :: PrimOp '[ 'HReal ] 'HReal
    Acos  :: PrimOp '[ 'HReal ] 'HReal
    Atan  :: PrimOp '[ 'HReal ] 'HReal
    Sinh  :: PrimOp '[ 'HReal ] 'HReal
    Cosh  :: PrimOp '[ 'HReal ] 'HReal
    Tanh  :: PrimOp '[ 'HReal ] 'HReal
    Asinh :: PrimOp '[ 'HReal ] 'HReal
    Acosh :: PrimOp '[ 'HReal ] 'HReal
    Atanh :: PrimOp '[ 'HReal ] 'HReal


    -- -- Other Real\/Prob-valued operators
    -- N.B., we only give the safe\/exact versions here. The old
    -- more lenient versions now require explicit coercions. Some
    -- of those coercions are safe, but others are not. This way
    -- we're explicit about where things can fail.
    -- N.B., we also have @NatPow{'HReal} :: 'HReal -> 'HNat -> 'HReal@,
    -- but non-integer real powers of negative reals are not real numbers!
    -- TODO: may need @SafeFrom_@ in order to branch on the input
    -- in order to provide the old unsafe behavior.
    RealPow   :: PrimOp '[ 'HProb, 'HReal ] 'HProb
    Choose    :: PrimOp '[ 'HNat, 'HNat ] 'HNat
    -- ComplexPow :: PrimOp '[ 'HProb, 'HComplex ] 'HComplex
    -- is uniquely well-defined. Though we may want to implement
    -- it via @r**z = ComplexExp (z * RealLog r)@
    -- Defining @HReal -> HComplex -> HComplex@ requires either
    -- multivalued functions, or a choice of complex logarithm and
    -- making it discontinuous.
    Exp       :: PrimOp '[ 'HReal ] 'HProb
    Log       :: PrimOp '[ 'HProb ] 'HReal
    -- TODO: Log1p, Expm1
    Infinity  :: HIntegrable a -> PrimOp '[] a
    -- TODO: add Factorial as the appropriate type restriction of GammaFunc?
    GammaFunc :: PrimOp '[ 'HReal ] 'HProb
    BetaFunc  :: PrimOp '[ 'HProb, 'HProb ] 'HProb


    -- -- -- Here we have the /polymorphic/ operators

    -- -- HEq and HOrd operators
    -- TODO: equality doesn't make constructive sense on the reals...
    -- would it be better to constructivize our notion of total ordering?
    -- TODO: should we have LessEq as a primitive, rather than treating it as a macro?
    Equal :: !(HEq  a) -> PrimOp '[ a, a ] HBool
    Less  :: !(HOrd a) -> PrimOp '[ a, a ] HBool


    -- -- HSemiring operators (the non-n-ary ones)
    NatPow :: !(HSemiring a) -> PrimOp '[ a, 'HNat ] a
    -- TODO: would it help to have a specialized version for when
    -- we happen to know that the 'HNat is a Literal? Same goes for
    -- the other powers\/roots
    --
    -- TODO: add a specialized version which returns NonNegative
    -- when the power is even? N.B., be sure not to actually constrain
    -- it to HRing (necessary for calling it \"NonNegative\")

    -- -- HRing operators
    -- TODO: break these apart into a hierarchy of classes. N.B,
    -- there are two different interpretations of "abs" and "signum".
    -- On the one hand we can think of rings as being generated
    -- from semirings closed under subtraction/negation. From this
    -- perspective we have abs as a projection into the underlying
    -- semiring, and signum as a projection giving us the residual
    -- sign lost by the abs projection. On the other hand, we have
    -- the view of "abs" as a norm (i.e., distance to the "origin
    -- point"), which is the more common perspective for complex
    -- numbers and vector spaces; and relatedly, we have "signum"
    -- as returning the value on the unit (hyper)sphere, of the
    -- normalized unit vector. In another class, if we have a notion
    -- of an "origin axis" then we can have a function Arg which
    -- returns the angle to that axis, and therefore define signum
    -- in terms of Arg.
    -- Ring: Semiring + negate, abs, signum
    -- NormedLinearSpace: LinearSpace + originPoint, norm, Arg
    -- ??: NormedLinearSpace + originAxis, angle
    Negate :: !(HRing a) -> PrimOp '[ a ] a
    Abs    :: !(HRing a) -> PrimOp '[ a ] (NonNegative a)
    -- cf., <https://mail.haskell.org/pipermail/libraries/2013-April/019694.html>
    -- cf., <https://en.wikipedia.org/wiki/Sign_function#Complex_signum>
    -- Should we have Maple5's \"csgn\" as well as the usual \"sgn\"?
    -- Also note that the \"generalized signum\" anticommutes with Dirac delta!
    Signum :: !(HRing a) -> PrimOp '[ a ] a
    -- Law: x = coerceTo_ signed (abs_ x) * signum x
    -- More strictly/exactly, the result of Signum should be either
    -- zero or an @a@-unit value. For Int and Real, the units are
    -- +1 and -1. For Complex, the units are any point on the unit
    -- circle. For vectors, the units are any unit vector. Thus,
    -- more generally:
    -- Law : x = coerceTo_ signed (abs_ x) `scaleBy` signum x
    -- TODO: would it be worth defining the associated type of unit values for @a@? Probably...
    -- TODO: are there any salient types which support abs\/norm but
    -- do not have all units and thus do not support signum\/normalize?


    -- Coecion-like operations that are computations
    -- we only implement Floor for Prob for now?
    Floor :: PrimOp '[ 'HProb ] 'HNat

    -- -- HFractional operators
    Recip :: !(HFractional a) -> PrimOp '[ a ] a
    -- generates macro: IntPow


    -- -- HRadical operators
    -- TODO: flip argument order to match our prelude's @thRootOf@?
    NatRoot :: !(HRadical a) -> PrimOp '[ a, 'HNat ] a
    -- generates macros: Sqrt, NonNegativeRationalPow, and RationalPow


    -- -- HContinuous operators
    -- TODO: what goes here, if anything? cf., <https://en.wikipedia.org/wiki/Closed-form_expression#Comparison_of_different_classes_of_expressions>
    Erf :: !(HContinuous a) -> PrimOp '[ a ] a
    -- TODO: make Pi and Infinity HContinuous-polymorphic so that we can avoid the explicit coercion? Probably more mess than benefit.


-- TODO: instance Read (PrimOp args a)
deriving instance Show (PrimOp args a)

instance JmEq2 PrimOp where
    jmEq2 :: PrimOp i1 j1 -> PrimOp i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2)
jmEq2 PrimOp i1 j1
Not         PrimOp i2 j2
Not         = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 PrimOp i1 j1
Impl        PrimOp i2 j2
Impl        = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 PrimOp i1 j1
Diff        PrimOp i2 j2
Diff        = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 PrimOp i1 j1
Nand        PrimOp i2 j2
Nand        = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 PrimOp i1 j1
Nor         PrimOp i2 j2
Nor         = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 PrimOp i1 j1
Pi          PrimOp i2 j2
Pi          = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 PrimOp i1 j1
Sin         PrimOp i2 j2
Sin         = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 PrimOp i1 j1
Cos         PrimOp i2 j2
Cos         = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 PrimOp i1 j1
Tan         PrimOp i2 j2
Tan         = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 PrimOp i1 j1
Asin        PrimOp i2 j2
Asin        = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 PrimOp i1 j1
Acos        PrimOp i2 j2
Acos        = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 PrimOp i1 j1
Atan        PrimOp i2 j2
Atan        = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 PrimOp i1 j1
Sinh        PrimOp i2 j2
Sinh        = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 PrimOp i1 j1
Cosh        PrimOp i2 j2
Cosh        = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 PrimOp i1 j1
Tanh        PrimOp i2 j2
Tanh        = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 PrimOp i1 j1
Asinh       PrimOp i2 j2
Asinh       = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 PrimOp i1 j1
Acosh       PrimOp i2 j2
Acosh       = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 PrimOp i1 j1
Atanh       PrimOp i2 j2
Atanh       = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 PrimOp i1 j1
RealPow     PrimOp i2 j2
RealPow     = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 PrimOp i1 j1
Exp         PrimOp i2 j2
Exp         = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 PrimOp i1 j1
Log         PrimOp i2 j2
Log         = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 PrimOp i1 j1
GammaFunc   PrimOp i2 j2
GammaFunc   = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 PrimOp i1 j1
BetaFunc    PrimOp i2 j2
BetaFunc    = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 (Equal HEq a
a)   (Equal HEq a
b)   =
        Sing a -> Sing a -> Maybe (TypeEq a a)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 (HEq a -> Sing a
forall (a :: Hakaru). HEq a -> Sing a
sing_HEq HEq a
a) (HEq a -> Sing a
forall (a :: Hakaru). HEq a -> Sing a
sing_HEq HEq a
b) Maybe (TypeEq a a)
-> (TypeEq a a -> Maybe (TypeEq i1 i2, TypeEq j1 j2))
-> Maybe (TypeEq i1 i2, TypeEq j1 j2)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq a a
Refl ->
        (TypeEq '[a, a] '[a, a],
 TypeEq
   ('HData ('TyCon "Bool") '[ '[], '[]])
   ('HData ('TyCon "Bool") '[ '[], '[]]))
-> Maybe
     (TypeEq '[a, a] '[a, a],
      TypeEq
        ('HData ('TyCon "Bool") '[ '[], '[]])
        ('HData ('TyCon "Bool") '[ '[], '[]]))
forall a. a -> Maybe a
Just (TypeEq '[a, a] '[a, a]
forall k (a :: k). TypeEq a a
Refl, TypeEq
  ('HData ('TyCon "Bool") '[ '[], '[]])
  ('HData ('TyCon "Bool") '[ '[], '[]])
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 (Less HOrd a
a)    (Less HOrd a
b)    =
        Sing a -> Sing a -> Maybe (TypeEq a a)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 (HOrd a -> Sing a
forall (a :: Hakaru). HOrd a -> Sing a
sing_HOrd HOrd a
a) (HOrd a -> Sing a
forall (a :: Hakaru). HOrd a -> Sing a
sing_HOrd HOrd a
b) Maybe (TypeEq a a)
-> (TypeEq a a -> Maybe (TypeEq i1 i2, TypeEq j1 j2))
-> Maybe (TypeEq i1 i2, TypeEq j1 j2)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq a a
Refl ->
        (TypeEq '[a, a] '[a, a],
 TypeEq
   ('HData ('TyCon "Bool") '[ '[], '[]])
   ('HData ('TyCon "Bool") '[ '[], '[]]))
-> Maybe
     (TypeEq '[a, a] '[a, a],
      TypeEq
        ('HData ('TyCon "Bool") '[ '[], '[]])
        ('HData ('TyCon "Bool") '[ '[], '[]]))
forall a. a -> Maybe a
Just (TypeEq '[a, a] '[a, a]
forall k (a :: k). TypeEq a a
Refl, TypeEq
  ('HData ('TyCon "Bool") '[ '[], '[]])
  ('HData ('TyCon "Bool") '[ '[], '[]])
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 (Infinity HIntegrable j1
a) (Infinity HIntegrable j2
b) =
        Sing j1 -> Sing j2 -> Maybe (TypeEq j1 j2)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 (HIntegrable j1 -> Sing j1
forall (a :: Hakaru). HIntegrable a -> Sing a
sing_HIntegrable HIntegrable j1
a) (HIntegrable j2 -> Sing j2
forall (a :: Hakaru). HIntegrable a -> Sing a
sing_HIntegrable HIntegrable j2
b) Maybe (TypeEq j1 j2)
-> (TypeEq j1 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2))
-> Maybe (TypeEq i1 i2, TypeEq j1 j2)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq j1 j2
Refl ->
        (TypeEq '[] '[], TypeEq j1 j1)
-> Maybe (TypeEq '[] '[], TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq '[] '[]
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 (NatPow   HSemiring j1
a) (NatPow   HSemiring j2
b) = HSemiring j1 -> HSemiring j2 -> Maybe (TypeEq j1 j2)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 HSemiring j1
a HSemiring j2
b Maybe (TypeEq j1 j2)
-> (TypeEq j1 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2))
-> Maybe (TypeEq i1 i2, TypeEq j1 j2)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq j1 j2
Refl -> (TypeEq '[j1, 'HNat] '[j1, 'HNat], TypeEq j1 j1)
-> Maybe (TypeEq '[j1, 'HNat] '[j1, 'HNat], TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq '[j1, 'HNat] '[j1, 'HNat]
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 (Negate   HRing j1
a) (Negate   HRing j2
b) = HRing j1 -> HRing j2 -> Maybe (TypeEq j1 j2)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 HRing j1
a HRing j2
b Maybe (TypeEq j1 j2)
-> (TypeEq j1 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2))
-> Maybe (TypeEq i1 i2, TypeEq j1 j2)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq j1 j2
Refl -> (TypeEq '[j1] '[j1], TypeEq j1 j1)
-> Maybe (TypeEq '[j1] '[j1], TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq '[j1] '[j1]
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 (Abs      HRing a
a) (Abs      HRing a
b) = HRing a -> HRing a -> Maybe (TypeEq a a)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 HRing a
a HRing a
b Maybe (TypeEq a a)
-> (TypeEq a a -> Maybe (TypeEq i1 i2, TypeEq j1 j2))
-> Maybe (TypeEq i1 i2, TypeEq j1 j2)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq a a
Refl -> (TypeEq '[a] '[a], TypeEq j1 j1)
-> Maybe (TypeEq '[a] '[a], TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq '[a] '[a]
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 (Signum   HRing j1
a) (Signum   HRing j2
b) = HRing j1 -> HRing j2 -> Maybe (TypeEq j1 j2)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 HRing j1
a HRing j2
b Maybe (TypeEq j1 j2)
-> (TypeEq j1 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2))
-> Maybe (TypeEq i1 i2, TypeEq j1 j2)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq j1 j2
Refl -> (TypeEq '[j1] '[j1], TypeEq j1 j1)
-> Maybe (TypeEq '[j1] '[j1], TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq '[j1] '[j1]
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 (Recip    HFractional j1
a) (Recip    HFractional j2
b) = HFractional j1 -> HFractional j2 -> Maybe (TypeEq j1 j2)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 HFractional j1
a HFractional j2
b Maybe (TypeEq j1 j2)
-> (TypeEq j1 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2))
-> Maybe (TypeEq i1 i2, TypeEq j1 j2)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq j1 j2
Refl -> (TypeEq '[j1] '[j1], TypeEq j1 j1)
-> Maybe (TypeEq '[j1] '[j1], TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq '[j1] '[j1]
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 (NatRoot  HRadical j1
a) (NatRoot  HRadical j2
b) = HRadical j1 -> HRadical j2 -> Maybe (TypeEq j1 j2)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 HRadical j1
a HRadical j2
b Maybe (TypeEq j1 j2)
-> (TypeEq j1 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2))
-> Maybe (TypeEq i1 i2, TypeEq j1 j2)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq j1 j2
Refl -> (TypeEq '[j1, 'HNat] '[j1, 'HNat], TypeEq j1 j1)
-> Maybe (TypeEq '[j1, 'HNat] '[j1, 'HNat], TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq '[j1, 'HNat] '[j1, 'HNat]
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 (Erf      HContinuous j1
a) (Erf      HContinuous j2
b) = HContinuous j1 -> HContinuous j2 -> Maybe (TypeEq j1 j2)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 HContinuous j1
a HContinuous j2
b Maybe (TypeEq j1 j2)
-> (TypeEq j1 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2))
-> Maybe (TypeEq i1 i2, TypeEq j1 j2)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq j1 j2
Refl -> (TypeEq '[j1] '[j1], TypeEq j1 j1)
-> Maybe (TypeEq '[j1] '[j1], TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq '[j1] '[j1]
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 PrimOp i1 j1
_ PrimOp i2 j2
_ = Maybe (TypeEq i1 i2, TypeEq j1 j2)
forall a. Maybe a
Nothing

-- TODO: We could optimize this like we do for 'Literal'
instance Eq2 PrimOp where
    eq2 :: PrimOp i j -> PrimOp i j -> Bool
eq2 PrimOp i j
x PrimOp i j
y = Bool
-> ((TypeEq i i, TypeEq j j) -> Bool)
-> Maybe (TypeEq i i, TypeEq j j)
-> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Bool -> (TypeEq i i, TypeEq j j) -> Bool
forall a b. a -> b -> a
const Bool
True) (PrimOp i j -> PrimOp i j -> Maybe (TypeEq i i, TypeEq j j)
forall k1 k2 (a :: k1 -> k2 -> *) (i1 :: k1) (j1 :: k2) (i2 :: k1)
       (j2 :: k2).
JmEq2 a =>
a i1 j1 -> a i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2)
jmEq2 PrimOp i j
x PrimOp i j
y)

instance Eq1 (PrimOp args) where
    eq1 :: PrimOp args i -> PrimOp args i -> Bool
eq1 = PrimOp args i -> PrimOp args i -> Bool
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Eq2 a =>
a i j -> a i j -> Bool
eq2

instance Eq (PrimOp args a) where -- This one can be derived
    == :: PrimOp args a -> PrimOp args a -> Bool
(==) = PrimOp args a -> PrimOp args a -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1

----------------------------------------------------------------
-- | Primitive operators for consuming or transforming arrays.
--
-- TODO: we may want to replace the 'Sing' arguments with something
-- more specific in order to capture any restrictions on what can
-- be stored in an array. Or, if we can get rid of them entirely
-- while still implementing all the use sites of
-- 'Language.Hakaru.Syntax.AST.Sing.sing_ArrayOp', that'd be
-- better still.
data ArrayOp :: [Hakaru] -> Hakaru -> * where
    -- HACK: is there any way we can avoid storing the Sing values here, while still implementing 'sing_PrimOp'?
    Index  :: !(Sing a) -> ArrayOp '[ 'HArray a, 'HNat ] a
    Size   :: !(Sing a) -> ArrayOp '[ 'HArray a ] 'HNat
    -- The first argument should be a monoid, but we don't enforce
    -- that; it's the user's responsibility.
    Reduce :: !(Sing a) -> ArrayOp '[ a ':-> a ':-> a, a, 'HArray a ] a
    -- TODO: would it make sense to have a specialized version for when the first argument is some \"Op\", in order to avoid the need for lambdas?

-- TODO: instance Read (ArrayOp args a)
deriving instance Show (ArrayOp args a)

instance JmEq2 ArrayOp where
    jmEq2 :: ArrayOp i1 j1
-> ArrayOp i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2)
jmEq2 (Index  Sing j1
a) (Index  Sing j2
b) = Sing j1 -> Sing j2 -> Maybe (TypeEq j1 j2)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing j1
a Sing j2
b Maybe (TypeEq j1 j2)
-> (TypeEq j1 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2))
-> Maybe (TypeEq i1 i2, TypeEq j1 j2)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq j1 j2
Refl -> (TypeEq '[ 'HArray j1, 'HNat] '[ 'HArray j1, 'HNat], TypeEq j1 j1)
-> Maybe
     (TypeEq '[ 'HArray j1, 'HNat] '[ 'HArray j1, 'HNat], TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq '[ 'HArray j1, 'HNat] '[ 'HArray j1, 'HNat]
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 (Size   Sing a
a) (Size   Sing a
b) = Sing a -> Sing a -> Maybe (TypeEq a a)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing a
a Sing a
b Maybe (TypeEq a a)
-> (TypeEq a a -> Maybe (TypeEq i1 i2, TypeEq j1 j2))
-> Maybe (TypeEq i1 i2, TypeEq j1 j2)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq a a
Refl -> (TypeEq '[ 'HArray a] '[ 'HArray a], TypeEq 'HNat 'HNat)
-> Maybe (TypeEq '[ 'HArray a] '[ 'HArray a], TypeEq 'HNat 'HNat)
forall a. a -> Maybe a
Just (TypeEq '[ 'HArray a] '[ 'HArray a]
forall k (a :: k). TypeEq a a
Refl, TypeEq 'HNat 'HNat
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 (Reduce Sing j1
a) (Reduce Sing j2
b) = Sing j1 -> Sing j2 -> Maybe (TypeEq j1 j2)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing j1
a Sing j2
b Maybe (TypeEq j1 j2)
-> (TypeEq j1 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2))
-> Maybe (TypeEq i1 i2, TypeEq j1 j2)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq j1 j2
Refl -> (TypeEq
   '[ j1 ':-> (j1 ':-> j1), j1, 'HArray j1]
   '[ j1 ':-> (j1 ':-> j1), j1, 'HArray j1],
 TypeEq j1 j1)
-> Maybe
     (TypeEq
        '[ j1 ':-> (j1 ':-> j1), j1, 'HArray j1]
        '[ j1 ':-> (j1 ':-> j1), j1, 'HArray j1],
      TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq
  '[ j1 ':-> (j1 ':-> j1), j1, 'HArray j1]
  '[ j1 ':-> (j1 ':-> j1), j1, 'HArray j1]
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 ArrayOp i1 j1
_          ArrayOp i2 j2
_          = Maybe (TypeEq i1 i2, TypeEq j1 j2)
forall a. Maybe a
Nothing

-- TODO: We could optimize this like we do for 'Literal'
instance Eq2 ArrayOp where
    eq2 :: ArrayOp i j -> ArrayOp i j -> Bool
eq2 ArrayOp i j
x ArrayOp i j
y = Bool
-> ((TypeEq i i, TypeEq j j) -> Bool)
-> Maybe (TypeEq i i, TypeEq j j)
-> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Bool -> (TypeEq i i, TypeEq j j) -> Bool
forall a b. a -> b -> a
const Bool
True) (ArrayOp i j -> ArrayOp i j -> Maybe (TypeEq i i, TypeEq j j)
forall k1 k2 (a :: k1 -> k2 -> *) (i1 :: k1) (j1 :: k2) (i2 :: k1)
       (j2 :: k2).
JmEq2 a =>
a i1 j1 -> a i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2)
jmEq2 ArrayOp i j
x ArrayOp i j
y)

instance Eq1 (ArrayOp args) where
    eq1 :: ArrayOp args i -> ArrayOp args i -> Bool
eq1 = ArrayOp args i -> ArrayOp args i -> Bool
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Eq2 a =>
a i j -> a i j -> Bool
eq2

instance Eq (ArrayOp args a) where -- This one can be derived
    == :: ArrayOp args a -> ArrayOp args a -> Bool
(==) = ArrayOp args a -> ArrayOp args a -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1


----------------------------------------------------------------
-- | Primitive operators to produce, consume, or transform
-- distributions\/measures. This corresponds to the old @Mochastic@
-- class, except that 'MBind' and 'Superpose_' are handled elsewhere
-- since they are not simple operators. (Also 'Dirac' is handled
-- elsewhere since it naturally fits with 'MBind', even though it
-- is a siple operator.)
--
-- TODO: we may want to replace the 'Sing' arguments with something
-- more specific in order to capture any restrictions on what can
-- be a measure space (e.g., to exclude functions). Or, if we can
-- get rid of them entirely while still implementing all the use
-- sites of 'Language.Hakaru.Syntax.AST.Sing.sing_MeasureOp',
-- that'd be better still.
data MeasureOp :: [Hakaru] -> Hakaru -> * where
    -- We might consider making Lebesgue and Counting polymorphic,
    -- since their restrictions to HProb and HNat are perfectly
    -- valid primitive measures. However, there are many other
    -- restrictions on measures we may want to consider, so handling
    -- these two here would only complicate matters.
    Lebesgue    :: MeasureOp '[ 'HReal, 'HReal ] 'HReal
    Counting    :: MeasureOp '[]                 'HInt
    Categorical :: MeasureOp '[ 'HArray 'HProb ] 'HNat
    -- TODO: make Uniform polymorphic, so that if the two inputs
    -- are HProb then we know the measure must be over HProb too.
    -- More generally, if the first input is HProb (since the second
    -- input is assumed to be greater thant he first); though that
    -- would be a bit ugly IMO.
    Uniform     :: MeasureOp '[ 'HReal, 'HReal ] 'HReal
    Normal      :: MeasureOp '[ 'HReal, 'HProb ] 'HReal
    Poisson     :: MeasureOp '[ 'HProb         ] 'HNat
    Gamma       :: MeasureOp '[ 'HProb, 'HProb ] 'HProb
    Beta        :: MeasureOp '[ 'HProb, 'HProb ] 'HProb

-- TODO: instance Read (MeasureOp typs a)
deriving instance Show (MeasureOp typs a)

instance JmEq2 MeasureOp where
    jmEq2 :: MeasureOp i1 j1
-> MeasureOp i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2)
jmEq2 MeasureOp i1 j1
Lebesgue    MeasureOp i2 j2
Lebesgue    = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 MeasureOp i1 j1
Counting    MeasureOp i2 j2
Counting    = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 MeasureOp i1 j1
Categorical MeasureOp i2 j2
Categorical = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 MeasureOp i1 j1
Uniform     MeasureOp i2 j2
Uniform     = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 MeasureOp i1 j1
Normal      MeasureOp i2 j2
Normal      = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 MeasureOp i1 j1
Poisson     MeasureOp i2 j2
Poisson     = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 MeasureOp i1 j1
Gamma       MeasureOp i2 j2
Gamma       = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 MeasureOp i1 j1
Beta        MeasureOp i2 j2
Beta        = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 MeasureOp i1 j1
_           MeasureOp i2 j2
_           = Maybe (TypeEq i1 i2, TypeEq j1 j2)
forall a. Maybe a
Nothing

-- TODO: We could optimize this like we do for 'Literal'
instance Eq2 MeasureOp where
    eq2 :: MeasureOp i j -> MeasureOp i j -> Bool
eq2 MeasureOp i j
x MeasureOp i j
y = Bool
-> ((TypeEq i i, TypeEq j j) -> Bool)
-> Maybe (TypeEq i i, TypeEq j j)
-> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Bool -> (TypeEq i i, TypeEq j j) -> Bool
forall a b. a -> b -> a
const Bool
True) (MeasureOp i j -> MeasureOp i j -> Maybe (TypeEq i i, TypeEq j j)
forall k1 k2 (a :: k1 -> k2 -> *) (i1 :: k1) (j1 :: k2) (i2 :: k1)
       (j2 :: k2).
JmEq2 a =>
a i1 j1 -> a i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2)
jmEq2 MeasureOp i j
x MeasureOp i j
y)

instance Eq1 (MeasureOp typs) where
    eq1 :: MeasureOp typs i -> MeasureOp typs i -> Bool
eq1 = MeasureOp typs i -> MeasureOp typs i -> Bool
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Eq2 a =>
a i j -> a i j -> Bool
eq2

instance Eq (MeasureOp typs a) where -- This one can be derived
    == :: MeasureOp typs a -> MeasureOp typs a -> Bool
(==) = MeasureOp typs a -> MeasureOp typs a -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1


----------------------------------------------------------------
----------------------------------------------------------------
-- N.B., the precedence of (:$) must be lower than (:*).
-- N.B., if these are changed, then be sure to update the Show instances
infix  4 :$ -- Chosen to be at the same precedence as (<$>) rather than ($)

-- | The constructor of a @(':$')@ node in the 'Term'. Each of these
-- constructors denotes a \"normal\/standard\/basic\" syntactic
-- form (i.e., a generalized quantifier). In the literature, these
-- syntactic forms are sometimes called \"operators\", but we avoid
-- calling them that so as not to introduce confusion vs 'PrimOp'
-- etc. Instead we use the term \"operator\" to refer to any primitive
-- function or constant; that is, non-binding syntactic forms. Also
-- in the literature, the 'SCon' type itself is usually called the
-- \"signature\" of the term language. However, we avoid calling
-- it that since our 'Term' has constructors other than just @(:$)@,
-- so 'SCon' does not give a complete signature for our terms.
--
-- The main reason for breaking this type out and using it in
-- conjunction with @(':$')@ and 'SArgs' is so that we can easily
-- pattern match on /fully saturated/ nodes. For example, we want
-- to be able to match @MeasureOp_ Uniform :$ lo :* hi :* End@
-- without needing to deal with 'App_' nodes nor 'viewABT'.
data SCon :: [([Hakaru], Hakaru)] -> Hakaru -> * where
    -- BUG: haddock doesn't like annotations on GADT constructors
    -- <https://github.com/hakaru-dev/hakaru/issues/6>

    -- -- Standard lambda calculus stuff
    Lam_ :: SCon '[ '( '[ a ], b ) ] (a ':-> b)
    App_ :: SCon '[ LC (a ':-> b ), LC a ] b
    Let_ :: SCon '[ LC a, '( '[ a ], b ) ] b
    -- TODO: a general \"@letrec*@\" version of let-binding so we can have mutual recursion
    --
    -- TODO: if we decide to add arbitrary fixedpoints back in, we
    -- should probably prefer only recursive-functions:
    -- `SCon '[ '( '[ a ':-> b, a ], a ':-> b ) ] (a ':-> b)`
    -- over than the previous recursive-everything:
    -- `SCon '[ '( '[ a ], a ) ] a`
    -- Or, if we really want to guarantee soundness, then we should
    -- only have the inductive principles for each HData.

    -- -- Type munging
    CoerceTo_   :: !(Coercion a b) -> SCon '[ LC a ] b
    UnsafeFrom_ :: !(Coercion a b) -> SCon '[ LC b ] a
    -- TODO: add something like @SafeFrom_ :: Coercion a b -> abt b -> Term abt ('HMaybe a)@ so we can capture the safety of patterns like @if_ (0 <= x) (let x_ = unsafeFrom signed x in...) (...)@ Of course, since we're just going to do case analysis on the result; why not make it a binding form directly?
    -- TODO: we'll probably want some more general thing to capture these sorts of patterns. For example, in the default implementation of Uniform we see: @if_ (lo < x && x < hi) (... unsafeFrom_ signed (hi - lo) ...) (...)@

    -- HACK: we must add the constraints that 'LCs' and 'UnLCs' are inverses, so that we have those in scope when doing case analysis (e.g., in TypeCheck.hs).
    -- As for this file itself, we can get it to typecheck by using 'UnLCs' in the argument rather than 'LCs' in the result; trying to do things the other way results in type inference issues in the typeclass instances for 'SCon'
    PrimOp_
        :: (typs ~ UnLCs args, args ~ LCs typs)
        => !(PrimOp typs a) -> SCon args a
    ArrayOp_
        :: (typs ~ UnLCs args, args ~ LCs typs)
        => !(ArrayOp typs a) -> SCon args a
    MeasureOp_
        :: (typs ~ UnLCs args, args ~ LCs typs)
        => !(MeasureOp typs a) -> SCon args ('HMeasure a)

    Dirac :: SCon '[ LC a ] ('HMeasure a)

    MBind :: SCon
        '[ LC ('HMeasure a)
        ,  '( '[ a ], 'HMeasure b)
        ] ('HMeasure b)

    -- TODO: unify Plate and Chain as @sequence@ a~la traversable?
    Plate :: SCon 
        '[ LC 'HNat
        , '( '[ 'HNat ], 'HMeasure a)
        ] ('HMeasure ('HArray a))


    -- TODO: if we swap the order of arguments to 'Chain', we could
    -- change the functional argument to be a binding form in order
    -- to avoid the need for lambdas. It'd no longer be trivial to
    -- see 'Chain' as an instance of @sequence@, but might be worth
    -- it... Of course, we also need to handle the fact that it's
    -- an array of transition functions; i.e., we could do:
    -- > chain n s0 $ \i s -> do {...}
    Chain :: SCon
        '[ LC 'HNat, LC s
        , '( '[ s ],  'HMeasure (HPair a s))
        ] ('HMeasure (HPair ('HArray a) s))


    -- -- Continuous and discrete integration.
    -- TODO: make Integrate and Summate polymorphic, so that if the
    -- two inputs are HProb then we know the function must be over
    -- HProb\/HNat too. More generally, if the first input is HProb
    -- (since the second input is assumed to be greater than the
    -- first); though that would be a bit ugly IMO.
    Integrate
        :: SCon '[ LC 'HReal, LC 'HReal, '( '[ 'HReal ], 'HProb) ] 'HProb
    -- TODO: the high and low bounds *should* be HInt. The only reason we use HReal is so that we can have infinite summations. Once we figure out a way to handle infinite bounds here, we can make the switch

    Summate
        :: HDiscrete a
        -> HSemiring b
        -> SCon '[ LC a, LC a, '( '[ a ], b) ] b

    Product
        :: HDiscrete a
        -> HSemiring b
        -> SCon '[ LC a, LC a, '( '[ a ], b) ] b

    -- Internalized program transformations
    Transform_ :: !(Transform as x)
               -> SCon as x

deriving instance Eq   (SCon args a)
-- TODO: instance Read (SCon args a)
deriving instance Show (SCon args a)

----------------------------------------------------------------
-- | The generating functor for Hakaru ASTs. This type is given in
-- open-recursive form, where the first type argument gives the
-- recursive form. The recursive form @abt@ does not have exactly
-- the same kind as @Term abt@ because every 'Term' represents a
-- locally-closed term whereas the underlying @abt@ may bind some
-- variables.
data Term :: ([Hakaru] -> Hakaru -> *) -> Hakaru -> * where
    -- BUG: haddock doesn't like annotations on GADT constructors
    -- <https://github.com/hakaru-dev/hakaru/issues/6>

    -- Simple syntactic forms (i.e., generalized quantifiers)
    (:$) :: !(SCon args a) -> !(SArgs abt args) -> Term abt a

    -- N-ary operators
    NaryOp_ :: !(NaryOp a) -> !(Seq (abt '[] a)) -> Term abt a

    -- TODO: 'Literal_', 'Empty_', 'Array_', and 'Datum_' are generalized quantifiers (to the same extent that 'Ann_', 'CoerceTo_', and 'UnsafeFrom_' are). Should we move them into 'SCon' just for the sake of minimizing how much lives in 'Term'? Or are they unique enough to be worth keeping here?

    -- Literal\/Constant values
    Literal_ :: !(Literal a) -> Term abt a

    -- These two constructors are here rather than in 'ArrayOp' because 'Array_' is a binding form; though it also means they're together with the other intro forms like 'Literal_' and 'Datum_'.
    --
    -- TODO: should we add a @Sing a@ argument to avoid ambiguity of 'Empty_'?
    Empty_ :: !(Sing ('HArray a)) -> Term abt ('HArray a)
    Array_
        :: !(abt '[] 'HNat)
        -> !(abt '[ 'HNat ] a)
        -> Term abt ('HArray a)

    ArrayLiteral_
        :: [abt '[] a]
        -> Term abt ('HArray a)

    -- Constructor for Reducers
    Bucket
        :: !(abt '[] 'HNat)
        -> !(abt '[] 'HNat)
        -> Reducer abt '[] a
        -> Term abt a
           
    -- -- User-defined data types
    -- BUG: even though the 'Datum' type has a single constructor, we get a warning about not being able to UNPACK it in 'Datum_'... wtf?
    --
    -- A data constructor applied to some expressions. N.B., this
    -- definition only accounts for data constructors which are
    -- fully saturated. Unsaturated constructors will need to be
    -- eta-expanded.
    Datum_ :: !(Datum (abt '[]) (HData' t)) -> Term abt (HData' t)

    -- Generic case-analysis (via ABTs and Structural Focalization).
    Case_ :: !(abt '[] a) -> [Branch a abt b] -> Term abt b

    -- Linear combinations of measures.
    Superpose_
        :: L.NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
        -> Term abt ('HMeasure a)

    -- The zero measure
    Reject_ :: !(Sing ('HMeasure a)) -> Term abt ('HMeasure a)

----------------------------------------------------------------
-- N.B., having a @singTerm :: Term abt a -> Sing a@ doesn't make
-- sense: That's what 'inferType' is for, but not all terms can be
-- inferred; some must be checked... Similarly, we can't derive
-- Read, since that's what typechecking is all about.


-- | A newtype of @abt '[]@, because sometimes we need this in order
-- to give instances for things. In particular, this is often used
-- to derive the obvious @Foo1 (abt '[])@ instance from an underlying
-- @Foo2 abt@ instance. The primary motivating example is to give
-- the 'Datum_' branch of the @Show1 (Term abt)@ instance.
newtype LC_ (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru) =
    LC_ { LC_ abt a -> abt '[] a
unLC_ :: abt '[] a }

instance Show2 abt => Show1 (LC_ abt) where
    showsPrec1 :: Int -> LC_ abt i -> ShowS
showsPrec1 Int
p = Int -> abt '[] i -> ShowS
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
Int -> a i j -> ShowS
showsPrec2 Int
p (abt '[] i -> ShowS)
-> (LC_ abt i -> abt '[] i) -> LC_ abt i -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LC_ abt i -> abt '[] i
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
LC_ abt a -> abt '[] a
unLC_
    show1 :: LC_ abt i -> String
show1        = abt '[] i -> String
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
a i j -> String
show2        (abt '[] i -> String)
-> (LC_ abt i -> abt '[] i) -> LC_ abt i -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LC_ abt i -> abt '[] i
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
LC_ abt a -> abt '[] a
unLC_

-- Alas, these two instances require importing ABT.hs
-- HACK: these instances require -XUndecidableInstances
instance ABT Term abt => Coerce (LC_ abt) where
    coerceTo :: Coercion a b -> LC_ abt a -> LC_ abt b
coerceTo   Coercion a b
CNil LC_ abt a
e       = LC_ abt a
LC_ abt b
e
    coerceTo   Coercion a b
c    (LC_ abt '[] a
e) = abt '[] b -> LC_ abt b
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> LC_ abt a
LC_ (Term abt b -> abt '[] b
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Coercion a b -> SCon '[LC a] b
forall (a :: Hakaru) (b :: Hakaru). Coercion a b -> SCon '[LC a] b
CoerceTo_ Coercion a b
c SCon '[LC a] b -> SArgs abt '[LC a] -> Term abt b
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
       (abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ abt '[] a
e abt '[] a -> SArgs abt '[] -> SArgs abt '[LC a]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
       (a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* SArgs abt '[]
forall (abt :: [Hakaru] -> Hakaru -> *). SArgs abt '[]
End))

    coerceFrom :: Coercion a b -> LC_ abt b -> LC_ abt a
coerceFrom Coercion a b
CNil LC_ abt b
e       = LC_ abt a
LC_ abt b
e
    coerceFrom Coercion a b
c    (LC_ abt '[] b
e) = abt '[] a -> LC_ abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> LC_ abt a
LC_ (Term abt a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Coercion a b -> SCon '[LC b] a
forall (a :: Hakaru) (b :: Hakaru). Coercion a b -> SCon '[LC b] a
UnsafeFrom_ Coercion a b
c SCon '[LC b] a -> SArgs abt '[LC b] -> Term abt a
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
       (abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ abt '[] b
e abt '[] b -> SArgs abt '[] -> SArgs abt '[LC b]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
       (a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* SArgs abt '[]
forall (abt :: [Hakaru] -> Hakaru -> *). SArgs abt '[]
End))

instance ABT Term abt => Coerce (Term abt) where
    coerceTo :: Coercion a b -> Term abt a -> Term abt b
coerceTo   Coercion a b
CNil Term abt a
e = Term abt a
Term abt b
e
    coerceTo   Coercion a b
c    Term abt a
e = Coercion a b -> SCon '[LC a] b
forall (a :: Hakaru) (b :: Hakaru). Coercion a b -> SCon '[LC a] b
CoerceTo_ Coercion a b
c SCon '[LC a] b -> SArgs abt '[LC a] -> Term abt b
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
       (abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ Term abt a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn Term abt a
e abt '[] a -> SArgs abt '[] -> SArgs abt '[LC a]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
       (a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* SArgs abt '[]
forall (abt :: [Hakaru] -> Hakaru -> *). SArgs abt '[]
End

    coerceFrom :: Coercion a b -> Term abt b -> Term abt a
coerceFrom Coercion a b
CNil Term abt b
e = Term abt a
Term abt b
e
    coerceFrom Coercion a b
c    Term abt b
e = Coercion a b -> SCon '[LC b] a
forall (a :: Hakaru) (b :: Hakaru). Coercion a b -> SCon '[LC b] a
UnsafeFrom_ Coercion a b
c SCon '[LC b] a -> SArgs abt '[LC b] -> Term abt a
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
       (abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ Term abt b -> abt '[] b
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn Term abt b
e abt '[] b -> SArgs abt '[] -> SArgs abt '[LC b]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
       (a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* SArgs abt '[]
forall (abt :: [Hakaru] -> Hakaru -> *). SArgs abt '[]
End

instance Show2 abt => Show1 (Term abt) where
    showsPrec1 :: Int -> Term abt i -> ShowS
showsPrec1 Int
p Term abt i
t =
        case Term abt i
t of
        SCon args i
o :$ SArgs abt args
es ->
            Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
4)
                ( Int -> SCon args i -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec  (Int
pInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) SCon args i
o
                ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" :$ "
                ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> SArgs abt args -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1 (Int
pInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) SArgs abt args
es
                )
        NaryOp_ NaryOp i
o Seq (abt '[] i)
es ->
            Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9)
                ( String -> ShowS
showString String
"NaryOp_ "
                ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> NaryOp i -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec  Int
11 NaryOp i
o
                ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" "
                ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> ShowS -> ShowS
showParen Bool
True
                    ( String -> ShowS
showString String
"Seq.fromList "
                    ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [abt '[] i] -> ShowS
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
[a i j] -> ShowS
showList2 (Seq (abt '[] i) -> [abt '[] i]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Seq (abt '[] i)
es)
                    )
                )
        Literal_ Literal i
v       -> Int -> String -> Literal i -> ShowS
forall a. Show a => Int -> String -> a -> ShowS
showParen_0   Int
p String
"Literal_" Literal i
v
        Empty_ Sing ('HArray a)
_         -> String -> ShowS
showString      String
"Empty_"
        Array_ abt '[] 'HNat
e1 abt '[ 'HNat] a
e2     -> Int -> String -> abt '[] 'HNat -> abt '[ 'HNat] a -> ShowS
forall k4 k5 k6 k7 (a :: k4 -> k5 -> *) (b :: k6 -> k7 -> *)
       (i1 :: k4) (j1 :: k5) (i2 :: k6) (j2 :: k7).
(Show2 a, Show2 b) =>
Int -> String -> a i1 j1 -> b i2 j2 -> ShowS
showParen_22  Int
p String
"Array_" abt '[] 'HNat
e1 abt '[ 'HNat] a
e2
        ArrayLiteral_ [abt '[] a]
es -> Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) (String -> ShowS
showString String
"ArrayLiteral_" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [abt '[] a] -> ShowS
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
[a i j] -> ShowS
showList2 [abt '[] a]
es)
        Datum_ Datum (abt '[]) (HData' t)
d         -> Int -> String -> Datum (LC_ abt) (HData' t) -> ShowS
forall k (a :: k -> *) (i :: k).
Show1 a =>
Int -> String -> a i -> ShowS
showParen_1   Int
p String
"Datum_" ((forall (i :: Hakaru). abt '[] i -> LC_ abt i)
-> Datum (abt '[]) (HData' t) -> Datum (LC_ abt) (HData' t)
forall k1 k2 (f :: (k1 -> *) -> k2 -> *) (a :: k1 -> *)
       (b :: k1 -> *) (j :: k2).
Functor11 f =>
(forall (i :: k1). a i -> b i) -> f a j -> f b j
fmap11 forall (i :: Hakaru). abt '[] i -> LC_ abt i
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> LC_ abt a
LC_ Datum (abt '[]) (HData' t)
d)
        Case_  abt '[] a
e [Branch a abt i]
bs      ->
            Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9)
                ( String -> ShowS
showString String
"Case_ "
                ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> abt '[] a -> ShowS
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
Int -> a i j -> ShowS
showsPrec2 Int
11 abt '[] a
e
                ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" "
                ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Branch a abt i] -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => [a i] -> ShowS
showList1 [Branch a abt i]
bs
                )
        Bucket abt '[] 'HNat
_ abt '[] 'HNat
_ Reducer abt '[] i
_   -> String -> ShowS
showString String
"Bucket ..."
        Superpose_ NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
pes ->
            Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9)
                ( String -> ShowS
showString String
"Superpose_ "
                ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((abt '[] 'HProb, abt '[] ('HMeasure a)) -> ShowS)
-> [(abt '[] 'HProb, abt '[] ('HMeasure a))] -> ShowS
forall a. (a -> ShowS) -> [a] -> ShowS
showListWith
                    (\(abt '[] 'HProb
e1,abt '[] ('HMeasure a)
e2) -> [ShowS] -> ShowS
showTuple [abt '[] 'HProb -> ShowS
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
a i j -> ShowS
shows2 abt '[] 'HProb
e1, abt '[] ('HMeasure a) -> ShowS
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
a i j -> ShowS
shows2 abt '[] ('HMeasure a)
e2])
                    (NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
-> [(abt '[] 'HProb, abt '[] ('HMeasure a))]
forall a. NonEmpty a -> [a]
L.toList NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
pes)
                )
        Reject_ Sing ('HMeasure a)
_     -> String -> ShowS
showString      String
"Reject_"

instance Show2 abt => Show (Term abt a) where
    showsPrec :: Int -> Term abt a -> ShowS
showsPrec = Int -> Term abt a -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1
    show :: Term abt a -> String
show      = Term abt a -> String
forall k (a :: k -> *) (i :: k). Show1 a => a i -> String
show1


----------------------------------------------------------------
instance Functor21 Term where
    fmap21 :: (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i)
-> Term a j -> Term b j
fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f (SCon args j
o :$ SArgs a args
es)          = SCon args j
o SCon args j -> SArgs b args -> Term b j
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
       (abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i)
-> SArgs a args -> SArgs b args
forall k1 k2 k3 (f :: (k1 -> k2 -> *) -> k3 -> *)
       (a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3).
Functor21 f =>
(forall (h :: k1) (i :: k2). a h i -> b h i) -> f a j -> f b j
fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f SArgs a args
es
    fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f (NaryOp_    NaryOp j
o  Seq (a '[] j)
es) = NaryOp j -> Seq (b '[] j) -> Term b j
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
NaryOp a -> Seq (abt '[] a) -> Term abt a
NaryOp_    NaryOp j
o ((a '[] j -> b '[] j) -> Seq (a '[] j) -> Seq (b '[] j)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a '[] j -> b '[] j
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f Seq (a '[] j)
es)
    fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
_ (Literal_   Literal j
v)     = Literal j -> Term b j
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Literal a -> Term abt a
Literal_   Literal j
v
    fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
_ (Empty_ Sing ('HArray a)
t)         = Sing ('HArray a) -> Term b ('HArray a)
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Sing ('HArray a) -> Term abt ('HArray a)
Empty_ Sing ('HArray a)
t
    fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f (Array_     a '[] 'HNat
e1 a '[ 'HNat] a
e2) = b '[] 'HNat -> b '[ 'HNat] a -> Term b ('HArray a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] 'HNat -> abt '[ 'HNat] a -> Term abt ('HArray a)
Array_     (a '[] 'HNat -> b '[] 'HNat
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f a '[] 'HNat
e1) (a '[ 'HNat] a -> b '[ 'HNat] a
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f a '[ 'HNat] a
e2)
    fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f (ArrayLiteral_ [a '[] a]
es) = [b '[] a] -> Term b ('HArray a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
[abt '[] a] -> Term abt ('HArray a)
ArrayLiteral_ ((a '[] a -> b '[] a) -> [a '[] a] -> [b '[] a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a '[] a -> b '[] a
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f [a '[] a]
es)
    fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f (Datum_     Datum (a '[]) (HData' t)
d)     = Datum (b '[]) (HData' t) -> Term b (HData' t)
forall (abt :: [Hakaru] -> Hakaru -> *) (t :: HakaruCon).
Datum (abt '[]) (HData' t) -> Term abt (HData' t)
Datum_     ((forall (i :: Hakaru). a '[] i -> b '[] i)
-> Datum (a '[]) (HData' t) -> Datum (b '[]) (HData' t)
forall k1 k2 (f :: (k1 -> *) -> k2 -> *) (a :: k1 -> *)
       (b :: k1 -> *) (j :: k2).
Functor11 f =>
(forall (i :: k1). a i -> b i) -> f a j -> f b j
fmap11 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
forall (i :: Hakaru). a '[] i -> b '[] i
f Datum (a '[]) (HData' t)
d)
    fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f (Case_      a '[] a
e  [Branch a a j]
bs) = b '[] a -> [Branch a b j] -> Term b j
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
abt '[] a -> [Branch a abt b] -> Term abt b
Case_      (a '[] a -> b '[] a
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f a '[] a
e)  ((Branch a a j -> Branch a b j) -> [Branch a a j] -> [Branch a b j]
forall a b. (a -> b) -> [a] -> [b]
map ((forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i)
-> Branch a a j -> Branch a b j
forall k1 k2 k3 (f :: (k1 -> k2 -> *) -> k3 -> *)
       (a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3).
Functor21 f =>
(forall (h :: k1) (i :: k2). a h i -> b h i) -> f a j -> f b j
fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f) [Branch a a j]
bs)
    fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f (Bucket     a '[] 'HNat
b a '[] 'HNat
e Reducer a '[] j
r) = b '[] 'HNat -> b '[] 'HNat -> Reducer b '[] j -> Term b j
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] 'HNat -> abt '[] 'HNat -> Reducer abt '[] a -> Term abt a
Bucket (a '[] 'HNat -> b '[] 'HNat
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f a '[] 'HNat
b) (a '[] 'HNat -> b '[] 'HNat
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f a '[] 'HNat
e) ((forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i)
-> Reducer a '[] j -> Reducer b '[] j
forall k1 k2 k3 k4 (f :: (k1 -> k2 -> *) -> k3 -> k4 -> *)
       (a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3) (l :: k4).
Functor22 f =>
(forall (h :: k1) (i :: k2). a h i -> b h i) -> f a j l -> f b j l
fmap22 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f Reducer a '[] j
r)
    fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f (Superpose_ NonEmpty (a '[] 'HProb, a '[] ('HMeasure a))
pes)   = NonEmpty (b '[] 'HProb, b '[] ('HMeasure a))
-> Term b ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
-> Term abt ('HMeasure a)
Superpose_ (((a '[] 'HProb, a '[] ('HMeasure a))
 -> (b '[] 'HProb, b '[] ('HMeasure a)))
-> NonEmpty (a '[] 'HProb, a '[] ('HMeasure a))
-> NonEmpty (b '[] 'HProb, b '[] ('HMeasure a))
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
L.map (a '[] 'HProb -> b '[] 'HProb
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f (a '[] 'HProb -> b '[] 'HProb)
-> (a '[] ('HMeasure a) -> b '[] ('HMeasure a))
-> (a '[] 'HProb, a '[] ('HMeasure a))
-> (b '[] 'HProb, b '[] ('HMeasure a))
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** a '[] ('HMeasure a) -> b '[] ('HMeasure a)
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f) NonEmpty (a '[] 'HProb, a '[] ('HMeasure a))
pes)
    fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
_ (Reject_ Sing ('HMeasure a)
t)        = Sing ('HMeasure a) -> Term b ('HMeasure a)
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Sing ('HMeasure a) -> Term abt ('HMeasure a)
Reject_ Sing ('HMeasure a)
t


----------------------------------------------------------------
instance Foldable21 Term where
    foldMap21 :: (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m) -> Term a j -> m
foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f (SCon args j
_ :$ SArgs a args
es)          = (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m)
-> SArgs a args -> m
forall k1 k2 k3 (f :: (k1 -> k2 -> *) -> k3 -> *) m
       (a :: k1 -> k2 -> *) (j :: k3).
(Foldable21 f, Monoid m) =>
(forall (h :: k1) (i :: k2). a h i -> m) -> f a j -> m
foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f SArgs a args
es
    foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f (NaryOp_    NaryOp j
_  Seq (a '[] j)
es) = (a '[] j -> m) -> Seq (a '[] j) -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
F.foldMap a '[] j -> m
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f Seq (a '[] j)
es
    foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
_ (Literal_   Literal j
_)     = m
forall a. Monoid a => a
mempty
    foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
_ (Empty_     Sing ('HArray a)
_)     = m
forall a. Monoid a => a
mempty
    foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f (Array_     a '[] 'HNat
e1 a '[ 'HNat] a
e2) = a '[] 'HNat -> m
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f a '[] 'HNat
e1 m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` a '[ 'HNat] a -> m
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f a '[ 'HNat] a
e2
    foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f (ArrayLiteral_ [a '[] a]
es) = (a '[] a -> m) -> [a '[] a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
F.foldMap a '[] a -> m
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f [a '[] a]
es
    foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f (Datum_     Datum (a '[]) (HData' t)
d)     = (forall (i :: Hakaru). a '[] i -> m)
-> Datum (a '[]) (HData' t) -> m
forall k1 k2 (f :: (k1 -> *) -> k2 -> *) m (a :: k1 -> *)
       (j :: k2).
(Foldable11 f, Monoid m) =>
(forall (i :: k1). a i -> m) -> f a j -> m
foldMap11 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
forall (i :: Hakaru). a '[] i -> m
f Datum (a '[]) (HData' t)
d
    foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f (Case_      a '[] a
e  [Branch a a j]
bs) = a '[] a -> m
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f a '[] a
e m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` (Branch a a j -> m) -> [Branch a a j] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
F.foldMap ((forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m)
-> Branch a a j -> m
forall k1 k2 k3 (f :: (k1 -> k2 -> *) -> k3 -> *) m
       (a :: k1 -> k2 -> *) (j :: k3).
(Foldable21 f, Monoid m) =>
(forall (h :: k1) (i :: k2). a h i -> m) -> f a j -> m
foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f) [Branch a a j]
bs
    foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f (Bucket     a '[] 'HNat
b a '[] 'HNat
e Reducer a '[] j
r) = a '[] 'HNat -> m
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f a '[] 'HNat
b m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` a '[] 'HNat -> m
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f a '[] 'HNat
e m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m)
-> Reducer a '[] j -> m
forall k1 k2 k3 k4 (f :: (k1 -> k2 -> *) -> k3 -> k4 -> *) m
       (a :: k1 -> k2 -> *) (j :: k3) (l :: k4).
(Foldable22 f, Monoid m) =>
(forall (h :: k1) (i :: k2). a h i -> m) -> f a j l -> m
foldMap22 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f Reducer a '[] j
r
    foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f (Superpose_ NonEmpty (a '[] 'HProb, a '[] ('HMeasure a))
pes)   = (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m)
-> NonEmpty (a '[] 'HProb, a '[] ('HMeasure a)) -> m
forall k k m (f :: * -> *) (abt :: k -> k -> *) (xs :: k) (a :: k)
       (ys :: k) (b :: k).
(Monoid m, Foldable f) =>
(forall (h :: k) (i :: k). abt h i -> m)
-> f (abt xs a, abt ys b) -> m
foldMapPairs forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f NonEmpty (a '[] 'HProb, a '[] ('HMeasure a))
pes
    foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
_ (Reject_    Sing ('HMeasure a)
_)     = m
forall a. Monoid a => a
mempty

foldMapPairs
    :: (Monoid m, F.Foldable f)
    => (forall h i. abt h i -> m)
    -> f (abt xs a, abt ys b)
    -> m
foldMapPairs :: (forall (h :: k) (i :: k). abt h i -> m)
-> f (abt xs a, abt ys b) -> m
foldMapPairs forall (h :: k) (i :: k). abt h i -> m
f = ((abt xs a, abt ys b) -> m) -> f (abt xs a, abt ys b) -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
F.foldMap (((abt xs a, abt ys b) -> m) -> f (abt xs a, abt ys b) -> m)
-> ((abt xs a, abt ys b) -> m) -> f (abt xs a, abt ys b) -> m
forall a b. (a -> b) -> a -> b
$ \(abt xs a
e1,abt ys b
e2) -> abt xs a -> m
forall (h :: k) (i :: k). abt h i -> m
f abt xs a
e1 m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` abt ys b -> m
forall (h :: k) (i :: k). abt h i -> m
f abt ys b
e2


----------------------------------------------------------------
instance Traversable21 Term where
    traverse21 :: (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i))
-> Term a j -> f (Term b j)
traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f (SCon args j
o :$ SArgs a args
es)          = (SCon args j
o SCon args j -> SArgs b args -> Term b j
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
       (abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$) (SArgs b args -> Term b j) -> f (SArgs b args) -> f (Term b j)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i))
-> SArgs a args -> f (SArgs b args)
forall k1 k2 k3 (t :: (k1 -> k2 -> *) -> k3 -> *) (f :: * -> *)
       (a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3).
(Traversable21 t, Applicative f) =>
(forall (h :: k1) (i :: k2). a h i -> f (b h i))
-> t a j -> f (t b j)
traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f SArgs a args
es
    traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f (NaryOp_    NaryOp j
o  Seq (a '[] j)
es) = NaryOp j -> Seq (b '[] j) -> Term b j
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
NaryOp a -> Seq (abt '[] a) -> Term abt a
NaryOp_  NaryOp j
o (Seq (b '[] j) -> Term b j) -> f (Seq (b '[] j)) -> f (Term b j)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a '[] j -> f (b '[] j)) -> Seq (a '[] j) -> f (Seq (b '[] j))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a '[] j -> f (b '[] j)
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f Seq (a '[] j)
es
    traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
_ (Literal_   Literal j
v)     = Term b j -> f (Term b j)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term b j -> f (Term b j)) -> Term b j -> f (Term b j)
forall a b. (a -> b) -> a -> b
$ Literal j -> Term b j
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Literal a -> Term abt a
Literal_ Literal j
v
    traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
_ (Empty_     Sing ('HArray a)
typ)   = Term b ('HArray a) -> f (Term b ('HArray a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term b ('HArray a) -> f (Term b ('HArray a)))
-> Term b ('HArray a) -> f (Term b ('HArray a))
forall a b. (a -> b) -> a -> b
$ Sing ('HArray a) -> Term b ('HArray a)
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Sing ('HArray a) -> Term abt ('HArray a)
Empty_   Sing ('HArray a)
typ
    traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f (Array_     a '[] 'HNat
e1 a '[ 'HNat] a
e2) = b '[] 'HNat -> b '[ 'HNat] a -> Term b ('HArray a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] 'HNat -> abt '[ 'HNat] a -> Term abt ('HArray a)
Array_ (b '[] 'HNat -> b '[ 'HNat] a -> Term b ('HArray a))
-> f (b '[] 'HNat) -> f (b '[ 'HNat] a -> Term b ('HArray a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a '[] 'HNat -> f (b '[] 'HNat)
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f a '[] 'HNat
e1 f (b '[ 'HNat] a -> Term b ('HArray a))
-> f (b '[ 'HNat] a) -> f (Term b ('HArray a))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a '[ 'HNat] a -> f (b '[ 'HNat] a)
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f a '[ 'HNat] a
e2
    traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f (ArrayLiteral_ [a '[] a]
es) = [b '[] a] -> Term b ('HArray a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
[abt '[] a] -> Term abt ('HArray a)
ArrayLiteral_ ([b '[] a] -> Term b ('HArray a))
-> f [b '[] a] -> f (Term b ('HArray a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a '[] a -> f (b '[] a)) -> [a '[] a] -> f [b '[] a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a '[] a -> f (b '[] a)
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f [a '[] a]
es
    traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f (Bucket a '[] 'HNat
b a '[] 'HNat
e Reducer a '[] j
r)     = b '[] 'HNat -> b '[] 'HNat -> Reducer b '[] j -> Term b j
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] 'HNat -> abt '[] 'HNat -> Reducer abt '[] a -> Term abt a
Bucket (b '[] 'HNat -> b '[] 'HNat -> Reducer b '[] j -> Term b j)
-> f (b '[] 'HNat)
-> f (b '[] 'HNat -> Reducer b '[] j -> Term b j)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a '[] 'HNat -> f (b '[] 'HNat)
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f a '[] 'HNat
b f (b '[] 'HNat -> Reducer b '[] j -> Term b j)
-> f (b '[] 'HNat) -> f (Reducer b '[] j -> Term b j)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a '[] 'HNat -> f (b '[] 'HNat)
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f a '[] 'HNat
e f (Reducer b '[] j -> Term b j)
-> f (Reducer b '[] j) -> f (Term b j)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i))
-> Reducer a '[] j -> f (Reducer b '[] j)
forall k1 k2 k3 k4 (t :: (k1 -> k2 -> *) -> k3 -> k4 -> *)
       (f :: * -> *) (a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3)
       (l :: k4).
(Traversable22 t, Applicative f) =>
(forall (h :: k1) (i :: k2). a h i -> f (b h i))
-> t a j l -> f (t b j l)
traverse22 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f Reducer a '[] j
r
    traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f (Datum_     Datum (a '[]) (HData' t)
d)     = Datum (b '[]) (HData' t) -> Term b j
forall (abt :: [Hakaru] -> Hakaru -> *) (t :: HakaruCon).
Datum (abt '[]) (HData' t) -> Term abt (HData' t)
Datum_ (Datum (b '[]) (HData' t) -> Term b j)
-> f (Datum (b '[]) (HData' t)) -> f (Term b j)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (i :: Hakaru). a '[] i -> f (b '[] i))
-> Datum (a '[]) (HData' t) -> f (Datum (b '[]) (HData' t))
forall k1 k2 (t :: (k1 -> *) -> k2 -> *) (f :: * -> *)
       (a :: k1 -> *) (b :: k1 -> *) (j :: k2).
(Traversable11 t, Applicative f) =>
(forall (i :: k1). a i -> f (b i)) -> t a j -> f (t b j)
traverse11 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
forall (i :: Hakaru). a '[] i -> f (b '[] i)
f Datum (a '[]) (HData' t)
d
    traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f (Case_      a '[] a
e  [Branch a a j]
bs) = b '[] a -> [Branch a b j] -> Term b j
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
abt '[] a -> [Branch a abt b] -> Term abt b
Case_  (b '[] a -> [Branch a b j] -> Term b j)
-> f (b '[] a) -> f ([Branch a b j] -> Term b j)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a '[] a -> f (b '[] a)
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f a '[] a
e f ([Branch a b j] -> Term b j) -> f [Branch a b j] -> f (Term b j)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Branch a a j -> f (Branch a b j))
-> [Branch a a j] -> f [Branch a b j]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i))
-> Branch a a j -> f (Branch a b j)
forall k1 k2 k3 (t :: (k1 -> k2 -> *) -> k3 -> *) (f :: * -> *)
       (a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3).
(Traversable21 t, Applicative f) =>
(forall (h :: k1) (i :: k2). a h i -> f (b h i))
-> t a j -> f (t b j)
traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f) [Branch a a j]
bs
    traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f (Superpose_ NonEmpty (a '[] 'HProb, a '[] ('HMeasure a))
pes)   = NonEmpty (b '[] 'HProb, b '[] ('HMeasure a))
-> Term b ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
-> Term abt ('HMeasure a)
Superpose_ (NonEmpty (b '[] 'HProb, b '[] ('HMeasure a))
 -> Term b ('HMeasure a))
-> f (NonEmpty (b '[] 'HProb, b '[] ('HMeasure a)))
-> f (Term b ('HMeasure a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i))
-> NonEmpty (a '[] 'HProb, a '[] ('HMeasure a))
-> f (NonEmpty (b '[] 'HProb, b '[] ('HMeasure a)))
forall k k (f :: * -> *) (t :: * -> *) (abt1 :: k -> k -> *)
       (abt2 :: k -> k -> *) (xs :: k) (a :: k) (ys :: k) (b :: k).
(Applicative f, Traversable t) =>
(forall (h :: k) (i :: k). abt1 h i -> f (abt2 h i))
-> t (abt1 xs a, abt1 ys b) -> f (t (abt2 xs a, abt2 ys b))
traversePairs forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f NonEmpty (a '[] 'HProb, a '[] ('HMeasure a))
pes
    traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
_ (Reject_    Sing ('HMeasure a)
typ)   = Term b ('HMeasure a) -> f (Term b ('HMeasure a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term b ('HMeasure a) -> f (Term b ('HMeasure a)))
-> Term b ('HMeasure a) -> f (Term b ('HMeasure a))
forall a b. (a -> b) -> a -> b
$ Sing ('HMeasure a) -> Term b ('HMeasure a)
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Sing ('HMeasure a) -> Term abt ('HMeasure a)
Reject_  Sing ('HMeasure a)
typ

traversePairs
    :: (Applicative f, Traversable t)
    => (forall h i. abt1 h i -> f (abt2 h i))
    -> t (abt1 xs a, abt1 ys b)
    -> f (t (abt2 xs a, abt2 ys b))
traversePairs :: (forall (h :: k) (i :: k). abt1 h i -> f (abt2 h i))
-> t (abt1 xs a, abt1 ys b) -> f (t (abt2 xs a, abt2 ys b))
traversePairs forall (h :: k) (i :: k). abt1 h i -> f (abt2 h i)
f = ((abt1 xs a, abt1 ys b) -> f (abt2 xs a, abt2 ys b))
-> t (abt1 xs a, abt1 ys b) -> f (t (abt2 xs a, abt2 ys b))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (((abt1 xs a, abt1 ys b) -> f (abt2 xs a, abt2 ys b))
 -> t (abt1 xs a, abt1 ys b) -> f (t (abt2 xs a, abt2 ys b)))
-> ((abt1 xs a, abt1 ys b) -> f (abt2 xs a, abt2 ys b))
-> t (abt1 xs a, abt1 ys b)
-> f (t (abt2 xs a, abt2 ys b))
forall a b. (a -> b) -> a -> b
$ \(abt1 xs a
x,abt1 ys b
y) -> (,) (abt2 xs a -> abt2 ys b -> (abt2 xs a, abt2 ys b))
-> f (abt2 xs a) -> f (abt2 ys b -> (abt2 xs a, abt2 ys b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> abt1 xs a -> f (abt2 xs a)
forall (h :: k) (i :: k). abt1 h i -> f (abt2 h i)
f abt1 xs a
x f (abt2 ys b -> (abt2 xs a, abt2 ys b))
-> f (abt2 ys b) -> f (abt2 xs a, abt2 ys b)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> abt1 ys b -> f (abt2 ys b)
forall (h :: k) (i :: k). abt1 h i -> f (abt2 h i)
f abt1 ys b
y

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