[<<][compsci][>>][..]

Sun Aug 21 09:41:35 CEST 2011

ArrowApply and ArrowMonad

As mentioned in the last post[1], it's not possible to use that
approach because you can't express compatibility of states in bind.
However, it is possible to make an Arrow instance which has
composition.

What I find here in Felipe's post[2] is that it is possible to create
the associated Monad[3] when making an instance of ArrrowApply[4].  So
it should not be possible to do so, or it's not really isomorphic, or
my previous explanation in [1] is wrong.

ArrowApply[4] generalizes ((a -> b), a) -> b, which is a curried form
of (a -> b) -> a -> b, from functions (->) to Arrows (-->), as an
arrow that applies another arrow to an input ((a --> b), a) --> b.

I tried to write it down but the wrapping confuses me.  First, what
does this mean in terms of non-wrapped types?

  a --> b               ==   a -> s -> (s, b)
  ((a --> b), a)        ==   ((a -> s -> (s, b)), a)

  ((a --> b), a) --> b  ==   ((a -> s -> (s, b)), a) -> s -> (s, b)

For the wrapped types this gives a very straightforward definition

  data Kl i o = forall s. Kl (i -> s -> (s, o))

  instance ArrowApply Kl where
    app = Kl $ \((Kl f), a) -> f a

However, it doesn't type-check.  The construction of app requires the
hidden type to be fixed when app is defined.  However, this type
depends on the _behaviour_ of app just as in [1], so there is a
dependency problem which is what the error message is trying to say:

    Couldn't match type `s0' with `s'
      because type variable `s' would escape its scope
    This (rigid, skolem) type variable is bound by
      a pattern with constructor
        Kl :: forall i o s. (i -> s -> (s, o)) -> Kl i o,
      in a lambda abstraction
    In the pattern: Kl f
    In the pattern: ((Kl f), a)
    In the second argument of `($)', namely `\ ((Kl f), a) -> f a'


                              * * *

The bottom line in this whole discussion seems to be that these 2
types are different:

    forall i o. (forall s. (i -> s -> (s, o)))
    forall i o. (i -> (forall s. s -> (s, o)))

In the latter the type s can depend on the value of i while in the
former it cannot.


[1] entry://20110820-221428
[2] http://www.mail-archive.com/haskell-cafe@haskell.org/msg92643.html
[3] http://hackage.haskell.org/packages/archive/base/4.3.1.0/doc/html/Control-Arrow.html#t:ArrowMonad
[4] http://hackage.haskell.org/packages/archive/base/4.3.1.0/doc/html/Control-Arrow.html#t:ArrowApply
[5] entry://20110821-123701

[Reply][About]

[<<][compsci][>>][..]