I've now almost got a FD solution to this problem, except that it won't work, and I don't know why. Of course, it's possible that the AT solution won't work either (I'm still compiling ghc, should have it in the morning...), but at least it seems far simpler. My FD solution is below. My trouble is that I really don't understand the limitations on FDs, which as I understand it is why Simon P.J. opposes adding them to Haskell': they're hard to understand. This all seems to work (although you'll see that I was reduced to using unsafeCoerce# in the IO instance, which is embarrassing--to say the least--but not unsafe), until I hit the RealWitness instance at the bottom, at which point ghc bombs out with: Witness.hs:33:0: Couldn't match expected type `m'' (a rigid variable) against inferred type `RealWitness a a'' `m'' is bound by the type signature for `>>' at Witness.hs:11:29 When using functional dependencies to combine Witness WitnessReally a b (RealWitness a b), (and a screenful more) Any suggestions? {-# OPTIONS -fno-implicit-prelude -fglasgow-exts #-} module Witness ( Witness ) where import GHC.Exts (unsafeCoerce#) import Prelude hiding ( (>>), (>>=), return, fail ) import qualified Prelude as P ( (>>), (>>=), return, fail ) class Witness w a b m | w a b -> m, m -> w a b where (>>=) :: (Witness w a a' m', Witness w a' b m'') => m' x -> (x -> m'' y) -> m y (>>) :: (Witness w a a' m', Witness w a' b m'') => m' x -> m'' y -> m y f >> g = f >>= const g private_return :: x -> m x fail :: String -> m x return :: Witness w a a m => x -> m x return = private_return data WitnessIO instance Witness WitnessIO () () IO where private_return = P.return fail = P.fail f >>= g = x2io f P.>>= y2io g where x2io :: Witness WitnessIO a b m => m x -> IO x x2io = unsafeCoerce# y2io :: Witness WitnessIO a b m => (y -> m x) -> (y -> IO x) y2io = unsafeCoerce# data RealWitness a b c -- this would be concrete data WitnessReally instance Witness WitnessReally a b (RealWitness a b) where {- The following monad is what I'd like to define if I could use associated type synonyms: class Witness w where type W w a b (>>=) :: W w a b x -> (x -> W w b c y) -> W w a c y (>>) :: W w a b x -> W w b c y -> W w a c y f >> g = f >>= const g return :: x -> W w a a x fail :: String -> W w a b x instance Monad m => Witness m where W m a b = m (>>=) = Prelude.(>>=) (>>) = Prelude.(>>) return = Prelude.return fail = Prelude.fail -}

On the FD impasse:

Witness.hs:33:0: Couldn't match expected type `m'' (a rigid variable) against inferred type `RealWitness a a'' `m'' is bound by the type signature for `>>' at Witness.hs:11:29 When using functional dependencies to combine Witness WitnessReally a b (RealWitness a b), (and a screenful more)

Any suggestions?

What follows isn't so much a suggestion, but I think it's a description of this error's origins. Note that >>='s signature from the class declaration

class Witness w a b m | w a b -> m, m -> w a b where (>>=) :: (Witness w a a' m', Witness w a' b m'') => m' x -> (x -> m'' y) -> m y (>>) :: (Witness w a a' m', Witness w a' b m'') => m' x -> m'' y -> m y f >> g = f >>= const g private_return :: x -> m x fail :: String -> m x

is "copied" to this instance declaration,

instance Witness WitnessReally a b (RealWitness a b) where

so we have: (>>=) :: ( Witness WitnessReally a a' m' , Witness WitnessReally a' b m'' ) => m' x -> (x -> m'' y) -> (RealWitness a b) y Now consider what the signature of >>= for this instance would be if this "copy from the class to the instance" operation were savvy to our plans: (>>=) :: ( Witness WitnessReally a a' (RealWitness a a') , Witness WitnessReally a' b (RealWitness a' b) ) => (RealWitness a a') x -> (x -> (RealWitness a' b) y) -> (RealWitness a b) y This signature is what the FD analyzer determines. Our above error arises because the actual signature of >>= has m' where the FDs indicate we'll always have (RealWitness a a'). Does that seem accurate? (I've put off actually looking at the GHC source for ages now...) In my opinion, this is reminiscent of some of the scoped-type variable issues and notions (e.g. wobbly types). By the functional dependency |w a b -> m|, we know that the m' and m'' in the signature of >>= will be determined as some particular types (i.e. the class is a type function from w a b to m), and we'd just like to refer to whatever those types actually are as m' and m''. It seems the FD analyzer determines for us what those particular types are, but then the type-checker is unhappy that we're naming them m' and m'' when we should know more about them (e.g. that they have a RealWitness tycon). Unfortunately, we have no choice about the signature of >>= at the instance declaration, since it's copied straight from the class declaration. If m' and m'' were recognized as partially wobbly variables, then maybe this wouldn't be a problem. Or maybe wobbly types could be framed in terms of functional dependencies on a non-method's signature? (The rest might be off-topic.) This situation also conjures up some of my own confusion about FDs, the open world assumption, and "finalizing" a typeclass. One of my main confusions with FDs is how they play with the open world assumption. Another confusion is that just because your instance declarations satisfy the FDs of a class, they won't necessisarily allow the type inference engine to act in accord to those FDs. Sometimes you have to break a class's definition into ancillary classes, each with one of the FDs you want and appropriate instance declarations to drive the inference along those particular FDs. If you try to cram all of the FDs into one set of instance declarations, they tend to choke the FD analyzer. (I read FDs as "a b and c" determine "x y and z"; this is a description of the class's membership, but the FD analysis takes place on the instance declarations themselves and not necessarily the types admitted to the class.) Nick

"Iavor Diatchki" wrote:

...

class IxMonad m where (>>>=) :: m i j a -> (a -> m j k b) -> m i k b ret :: a -> m i i a

And just for fun we can define another indexed monad: state that supports "strong updates" (i.e., the type of the state can change as you compute):

...

newtype State i j a = S { unS :: i -> (a,j) }

This reminded me very much of the state monad (actually more general than a monad) used internally in the nhc98/yhc compiler. Attached below. Niklas Rojemo came up with this formulation in 1993. Regards, Malcolm ---- module State where -- Use >>> and >>>= instead of >> and >>= to avoid problems with 1.3 prelude infixl 5 >>>,>>>=,=>>> infixr 4 >=> type State0 d s s' = d -> s -> s' type State d s u s' = d -> s -> (u,s') -- 'unit' is what is now known as 'return' in monad-speak unitS :: u -> State d s u s unitS u = (\d s -> (u,s)) unitS0 :: State0 d s s unitS0 = (\d s -> s) -- There are four 'bind'-like operators, >>>, >>>=, =>>>, and >=> (>>>) :: State0 d a b -> State0 d b c -> State0 d a c f >>> g = \d s -> g d (f d s) (=>>>) :: State d s (a->b) s' -> State d s' a s'' -> State d s b s'' f =>>> g = \d s -> case f d s of (h,s) -> case g d s of (x,s) -> let hx = h x in seq hx (hx,s) -- f =>>> g = \d s -> case f d s of (h,s) -> case g d s of (x,s) -> (h x,s) (>>>=) :: State d s a s' -> (a -> State0 d s' s'') -> State0 d s s'' f >>>= g = \d s -> case f d s of (x,s) -> g x d s (>=>) :: State d s d' s' -> State0 d' s' s'' -> State0 d s s'' f >=> g = \d s -> case f d s of (d,s) -> (g d s) mapS :: (a->State d s b s) -> [a] -> State d s [b] s mapS f [] = unitS [] mapS f (x:xs) = unitS (:) =>>> f x =>>> mapS f xs mapS0 :: (a->State0 d s s) -> [a] -> State0 d s s mapS0 f [] = unitS0 mapS0 f (x:xs) = f x >>> mapS0 f xs zipWithS :: (a -> b -> State d s c s) -> [a] -> [b] -> State d s [c] s zipWithS f [] [] = unitS [] zipWithS f (x:xs) (y:ys) = unitS (:) =>>> f x y =>>> zipWithS f xs ys zipWithS _ _ _ = error "zipWithS: lists of different lengths" ----

David Roundy wrote:

The trouble is that your solution doesn't allow you to use do-notation with the IxMonad. And if you did allow yourself to use do-notation by rebinding (>>=), etc, then you wouldn't be able to use ordinary monads with do-notation in the same module. That's what makes things tricky, since an IxMonad is different-kinded from Monad, so you can't make a monad an instance of IxMonad.

Seems to me that this screams for camlp4. Oops, wrong language ;-) But seriously, this kind of thing seems to arise often enough that having a standard method for doing "syntax extensions" for Haskell seems like a good idea. And as far as making Monad instances for IxMonad, this is where partial application at the class level would come in rather handy. Seems to be that (at least) IxMonad m () () should be a Monad. Jacques

First, I believe that this paper http://homepages.inf.ed.ac.uk/ratkey/param-notions.pdf is intimately related to WitnessMonad. David Roundy wrote:

Rebinding the do notation is at least reasonably clean, it's just that we don't want to lose the ability to mix with ordinary monads. This inability is what made me suggest an experimental syntax extension rather than rebinding.

I'm not sure that syntax extensions are very often a good idea...

I view syntax extensions as a proof-of-concept mechanism: you show that your new idea, if it had proper syntactic support, can make some kinds of programming a lot easier and clearer. Then hopefully the extension gets incorporated into official syntax. If not, then the extension should in time disappear. The main advantage is to make experiments (for new syntax) possible. Right now, the barriers to surmount for syntactic matters is quite high. I agree that it is rare that a syntax extension is really a "good" idea.

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.

Yes, if you can make that work, that is quite pretty. Jacques

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? It doesn't work with GHC head, and I can't really do anything about that. Mostly curiosity. Thanks pepe ---------------------------------------------------------------- Everything from here on is to convince GMane that, even if my message contains more quoted text than fresh text, it is a legitimate message and it should be ok to post it.

...

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.

Sorry I replied from gmane; I should have included a link to the original thread, but I really expected gmane to do that. The thread is at: http://www.haskell.org/pipermail/haskell-cafe/2006-December/020615.html

...

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:

I will try to fill in the details, but surely it is all expanded in the original thread. The idea is that we have an indexed/effectful monad where bind and return have a parameterized type: class WitnessMonad m where (>>=) :: m a b x -> (x -> m b c y) -> m a c y return :: x -> m a a x We can produce instances of WitnessMonad from an existing Monad using an adaptor newtype WitnessAdaptor m a b x = W {unW::m x} instance Monad m => WitnessMonad (WitnessAdaptor m) And rebind the do syntax to our WitnessMonad. But using vanilla Monads via this trick requires to lift and unlift every monadic action with the adaptor. An example in the IO monad: test1 :: IO String test1 = unW$ do msg <- W getLine W$ putStrLn "Thanks!" return msg From here on the intent was on producing a solution using ATs that hides this explicit wrapping. I don't really know the details of the proposed solution. Thanks pepe