[Haskell-cafe] Re: AT solution: rebinding >>= for restricted monads

[Manuel M T Chakravarty]

Pepe Iborra:
> David Roundy <droundy <at> darcs.net> writes:
> > My latest attemp (which won't compile with the HEAD ghc that I just compiled,
> > probably because I haven't figured out the synatax for guards with indexed
> > types is:
> > 
> > class WitnessMonad m where
> >     type W m :: * -> * -> *
> >     (>>=) :: (WitnessMonad m', WitnessMonad m'',
> >               w a b = W m', w b c = W m'', w a c = W m)
> >           => m' x -> (x -> m'' y) -> m y
> >     (>>) :: (WitnessMonad m', WitnessMonad m'',
> >               w a b = W m', w b c = W m'', w a c = W m)
> >           => m' x -> m'' y -> m y
> >     f >> g = f >>= const g
> >     return :: w a a = W m x => -> m x
> >     fail :: String -> m x
> > 
> > data Witness a b
> > 
> > instance Monad m => WitnessMonad m where
> >     W m = Witness () ()
> >     (>>=) = Prelude.(>>=)
> >     (>>) = Prelude.(>>)
> >     return = Prelude.return
> >     fail = Prelude.fail
> > 
> > which I think is quite pretty.  It allows the Monadlike object to have kind
> > * -> *, while still allowing us to hide extra witness types inside and pull
> > them out using the W function.
>
> Did anyone with knowledge of Associated Types pursue this solution? 

Where did you get this from.  My haskell-cafe mail folder doesn't seem
to have the thread you are replying to.

> It doesn't work with GHC head, and I can't really do anything about that.
> Mostly curiosity. 

The main reason this doesn't work with the head is because the
implementation of associated type *synonyms* (as opposed to associated
data types) is still incomplete.  (See also
<http://haskell.org/haskellwiki/GHC/Indexed_types>.)  We are working at
the implementation, but I just relocated from New York to Sydney, which
is why not much happened in the last two months. 

But I also don't quite understand the intention of this code:

* What exactly is the kind of the type function W supposed to be?  Is it
  "(* -> *) -> *"?  If so, then the declaration needs to be

    class WitnessMonad m where
      type W m :: *
      ....

  That is, assuming (m :: * -> *), we have (W m :: *) with (W :: (* -> 
  *) -> *).

* In the signature

    (>>=) :: (WitnessMonad m', WitnessMonad m'',
              w a b = W m', w b c = W m'', w a c = W m)

  what is the purpose of "w" (and hence the purpose of the equality 
  constraints)?  What you really want is to impose a kind of state 
  transition relationship on the monads involved in monad binds, right?

* In the instance, using Prelude.>>= for the witness monad won't work.
  After all, Prelude.>>= can only combine two actions in the same monad,
  but the WitnessMonad signature promises to combine two different
  WitnessMonads (under certain constraints).

* Another problem with the instance is that it requires undecidable 
  instances.

As I am not quite sure about the intention of the code it is hard to
propose a fix.  In particular, I have no idea how you want to combine
two different witness monads in (>>=).

Manuel