[Haskell-cafe] The semiring of Scott reals (Thoughts about redesigning "Num" type class)
olf at aatal-apotheke.de
Sun Sep 13 19:51:17 UTC 2015
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.
More information about the Haskell-Cafe