Monad instance trouble: Any way to implement unionWith on some kind of map type, without an Ord constraint?

Learn
#21

I have to say I am struggling to implement this and I think it’s all too abstract for me at my current level of knowledge.

Although I’ve explored further with this, the minimal problem is reproduced by this code, which is almost verbatim from the parent post:

type Probability = Float

class Monoid r => Cone r where
   scale :: Probability -> r -> r
   -- Monoid to be understood additively

type Dist a = forall r. Cone r => (a -> r) -> r

pure :: a -> Dist a
pure a = \b -> b a

bind :: (a -> Dist b) -> Dist a -> Dist b
bind k m = \b -> m (flip k b)

This gives the following error:

olf.hs:13:26: error: [GHC-83865]
    • Couldn't match type: forall r1. Cone r1 => (b -> r1) -> r1
                     with: (b -> r) -> r
      Expected: a -> (b -> r) -> r
        Actual: a -> Dist b
    • In the first argument of ‘flip’, namely ‘k’
      In the first argument of ‘m’, namely ‘(flip k b)’
      In the expression: m (flip k b)
    • Relevant bindings include
        b :: b -> r (bound at olf.hs:13:13)
        k :: a -> Dist b (bound at olf.hs:13:6)
        bind :: (a -> Dist b) -> Dist a -> Dist b (bound at olf.hs:13:1)
   |
13 | bind k m = \b -> m (flip k b)
   |                          ^

Maybe “maximally free” translates to “not actually typeable”, I don’t know!

It’s unclear to me how the Dist type is supposed to work, frankly, even the pure function.

As I say, I’ve explored further and keep failing, presumably due my misunderstanding of the model that’s being proposed.

Thanks for any help anyone can offer!

#22

Apologies, you need the RankNTypes language extension, which I neglected to include in the post. Apart from that, there was a change in type inference between GHC 8 and 9 that stops the code from type checking.
You can paste the code into the Haskell Playground and choose the compiler version. It will compile with GHC 8.
To satisfy GHC 9, we need the more involved:

{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}

type Dist a = forall r. Cone r => (a -> r) -> r

bind :: forall a b. (a -> Dist b) -> Dist a -> Dist b
bind k m = let
  flipk :: forall r. Cone r => (b -> r) -> a -> r
  flipk b a = k a b
  in m . flipk
#23

Okay, observe that bind k m = m . flip k where

flip k :: forall r. Cone r => (b -> r) -> (a -> r)

Now we specialize b=a since we want k :: a -> Dist a. This makes

flip k :: forall r. Cone r => (a -> r) -> (a -> r)

Now it is not hard to see that

bind k (bind k m) = (m . flip k) . flip k

or in terms of function composition

(bind k . bind k) m = m . (flip k . flip k)

By induction, iterating the bind k operator on any starting distribution m is the same as pre-composing the m functional with iterated compositions of flip k.
We may than ask whether there is a limit to this process. Apparently we need to compute the infinite composition of a function with itself. Suppose f :: x -> x (where in our case, x = (a -> r) but that does not matter for now). We need a function f_iterated with the property that

f_iterated = f . f_iterated

Hence

f_iterated x = f (f_iterated x)

Observe that f_iterated x obeys the same equation as fix f, namely

fix f = f (fix f)

whence we conclude that f_iterated x = fix f and thereby f_iterated = const (fix f).

EDIT: There is a problem with the above calculations. The Riesz embedding of distributions into continuations always produces linear continuations. If r is a cone, then the function space a -> r has (point-wise) cone structure. Thus we can talk about a functional phi :: (a -> r) -> r to preserve cone structure, in the sense that

  1. phi mempty = mempty
  2. phi (f <> g) = phi f <> phi g
  3. phi (scale p f) = scale p (phi f)

But even if flip k is linear by construction, its iterated limit const (fix (flip k)) needs not be linear unless it is a trivial function like constant bottom or constant mempty.
What we are missing here is a proof that the function bind k does possess a sensible fixed point at all. Recall that fix always computes the least fixed point, whereas e.g. bind pure (by monad laws) holds every distribution fixed.

#24

OK, Thanks for this.

So, if I want to define an instance of Dist – Dist String, say – I am perplexed that pure is so simple. I would expect any instance of Dist to involve a representation of a distribution, say [(String, Probability)]. I get that your definition of Dist uses a kind of CPS interface but I’m wondering where if anywhere code something like this would appear:

\m -> mconcat $ Prelude.map (\(x, p) -> scale p (m x)) d

where d is the [(String, Probability)].

It doesn’t seem to make sense that Dist a should be isomorphic to a single value of type a.

#25

We’re using the Riesz-Markov-Kakutani representation theorem here.
My implementation of Dist is representing the distribution by the way one can integrate functions against it. Consider the types in the mathematical expression ∫ f dμ. Integration takes a scalar-valued function f :: a -> r and a distribution μ and produces a scalar value. If we fix the distribution μ then this yields a continuation (a -> r) -> r.

The nice thing is that distributions themselves form a cone (and Dist an Alternative functor), whence we can use them as r in the universally-quantified variable.

-- <|> of the Alternative instance
addDists :: Dist a -> Dist a -> Dist a
addDists dx dy = \b -> dx b <> dy b

-- empty of the Alternative instance
zeroDist :: Dist a
zeroDist = const mempty

-- scale of the Cone instance
scaleDist :: Probability -> Dist a -> Dist a
scaleDist p dx = \b -> scale p (dx b)

This gives you all the tools to define an embedding of finite distributions:

fromFinDist :: (Cone (dist a), Alternative dist) => 
   [(Probability,a)] -> dist a
fromFinDist = foldr f empty where
    f (p,a) dx = (scale p (pure a)) <|> dx
1 Like
#26

That is because integration against a Dirac distribution is just function evaluation. If μ is the Dirac distribution with all mass (probability) concentrated at x, then ∫ f dμ = f(x).

1 Like