[Haskell-cafe] The semiring of Scott reals (Thoughts about redesigning "Num" type class)

[Mike Izbicki]

Two things:

1) My subhask library's reimplementation of the numeric hierarchy is
compatible with the Scott Reals you define.  It can be made an
instance of SubHask's Rig typeclass.  See
https://github.com/mikeizbicki/subhask/blob/master/src/SubHask/Algebra.hs#L1309-L1317

The trickiest thing I've found with numeric hierarchy rewrites is
handling units of measure properly.  There's a good discussion about
this on SubHask's issue tracker:
https://github.com/mikeizbicki/subhask/issues/11

2) WRT to integration, that's cool!  I hadn't thought of the
connection between integration and the bind operation before.

I think we can probably take it a step further.  When you talk about
the list monad "disregarding permutations", what you're actually
talking about is the set monad.  And now that I think about it, it
makes sense that bind on the set monad closely corresponds to the
traditional measure-theoretic view of integration on sets.  So the
interesting follow on question is: can we define integration on
non-set monads?

I've though a bit about defining integration on non-sets before.  My
approach (also used in subhask) was via the Foldable type class.  See
this Cafe thread for more details:
https://mail.haskell.org/pipermail/haskell-cafe/2015-March/118471.html

Something I haven't done is connect this with the monad instance for
the type we're integrating over... but now I'm definitely going to
look into it :)

On Sun, Sep 13, 2015 at 12:51 PM, Olaf Klinke <olf at aatal-apotheke.de> wrote:
> This departs somewhat from the thread's topic. Below I detail a semiring R that is not a ring because negation is not definable in Haskell. I further sketch integration in Haskell which I ripped off papers by Gordon Plotkin, Steve Vickers, Anders Kock and others.
>
> Infinity comes in as a limit, of course. Approximate a real number by an ascending stream of rational numbers. (The ascending can not be enforced by Haskell's type system, of course.). What you have is a so-called lower real or Scott real. Still addition and multiplication is continuous on such reals and there is a unique way of extending these operations to infinity, represented by any strictly ascending stream. Neither subtraction not division are computable for the Scott reals. Indeed, to know a lower bound of x-y one needs to know upper bounds of y. Denote this type by R:
>
> type R = Stream Rational
>
> Further consider ascending streams of Booleans, where any two streams containing True are considered semantically equivalent.
>
> type S = Stream Bool
>
> Consider the following types:
>
> type ScottOpen x = x -> S
> type V x = (ScottOpen x) -> R
>
> Certain elements of the type V x are called valuations, assigning to any Scott open subset[*] of x a lower real number. The type constructor V has a monad instance. If there was a one-element type in Haskell (say 1), then V 1 is isomorphic to R. Hence a lower semicontinuous real-valued function f :: x -> R is the same as a function f :: x -> V 1. Now observe that
>
>   (=<<) :: (x -> V 1) -> V x -> V 1
>         :: (x -> R  ) -> V x -> R
>
> has the type of an integral operator. In other words, the bind of the monad V implements integration. I have an implementation that lets you do integration over any Haskell type, but it is very slow.
>
> An analogue of this is the monad []. Indeed, total elements of type N = [()] are natural numbers. Disregarding permutations, an element of [x] assigns to finitely many elements of x a weight from the natural numbers. Then
>
>   (=<<) :: (x -> [()]) -> [x] -> [()]
>         :: (x -> N   ) -> [x] -> N
>
> is the integral operator integrating natural-number-valued functions against a finite natural-number-valued measure. Further observe that
>
>   liftM2 (flip const) :: Monad m => m () -> m x -> m x
>
> is a monoid action that implements multiplication on N. It distributes over (++) for categorical reasons: (++) arises from the isomorphism (up to permutation)
>
>    ([a],[b]) -> [Either a b].
>
> As an exercise, define a monad instance for
>
> type FinDist x = [(x,Rational)]
>
>     Hint: FinDist x = WriterT (Product Rational) [] x
>
> and observe that FinDist () is isomorphic to Rational (up to some equivalence relation). Voila: You have integration of Rational-valued functions against finitely supported distributions. For many combinatorial applications, this is sufficient.
>
> [*] For u :: x -> S, consider the set of elements of x for which u produces a stream containing True. This is the Scott open subset. Valuations are required to send the empty open to the constant zero stream and further obey the modular law you know from measures:
>
>   v(u) + v(u') = v(union u u') + v(intersection u u')
>
> where union = liftA2 max and intersection = liftA2 min.
>
> -- Olaf
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe