Sun Aug 21 09:41:35 CEST 2011
ArrowApply and ArrowMonad
As mentioned in the last post, 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
What I find here in Felipe's post is that it is possible to create
the associated Monad when making an instance of ArrrowApply. So
it should not be possible to do so, or it's not really isomorphic, or
my previous explanation in  is wrong.
ArrowApply 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 , 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.