Pepe Iborra:
David Roundy
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