Re: [Haskell-cafe] Re: AT solution: rebinding = for restricted monads
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: AT solution: rebinding = for restricted monads
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? 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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: AT solution: rebinding = for restricted monads
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe