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
