[Haskell-cafe] Help defining a Typeable polymorphic-state monad transformer

[Luke Palmer]

This has nothing to do with a monad.  This is just about data.  You
want a type that can contain any Typeable type, and a safe way to cast
out of that type into the type that came in.  Such a thing exists,
it's called Data.Dynamic.

Then your monad is just StateT Dynamic, where your magical maybeifying get is:

getD :: (Monad m, Typeable a) => StateT Dynamic m a
getD = maybe (fail "Type error") return . cast =<< get

Luke

On Mon, Dec 6, 2010 at 9:09 PM, Brandon Simmons
<brandon.m.simmons at gmail.com> wrote:
> Hi all,
>
> I gave myself until this evening to figure this out on my own, and
> time is up! Hopefully this makes for a good discussion, though the
> idea could be dumb.
>
> What I'm trying to do is define a state monad in which the passed
> state can change type during the computation. The only constraint is
> that the state types must always be of the Typeable class (see:
> http://hackage.haskell.org/packages/archive/base/latest/doc/html/Data-Typeable.html
> ).
>
> The idea is that the new monad would be something like 'StateT s Maybe
> a', but where the 's' type is not fixed (indeed is hidden in an
> existential type) and where any programmer errors in the chaining of
> the polymorphic state will be caught in the Maybe type (or really the
> 'fail' implementation of any monad).
>
> Here is how I imagine a computation might look:
>
>    computation :: TypeableState Maybe String
>    computation = do
>        (c:cs) <-  getTS
>        putTS (length cs)
>        return ("c" ++ " was the first letter of the string passed as
> initial state.")
>
> So TypeableState is very similar to StateT, except that the state type
> is not present as a type argument. In the example above 'Maybe' is the
> monad that catches Typeable errors, and String is the return type of
> the computation.
>
> getTS and putTS would be get and put functions that constrain their
> arguments to the Typeable class.
>
> Here is what I have so far (at least this is my most recent
> uncommented attempt):
>
>> {-# LANGUAGE ExistentialQuantification #-}
>> module Main
>>       where
>>
>> import Control.Monad.State
>> import Data.Typeable
>>
>> -- we might have restricted our 'm' to MonadPlus and used the explicit
>> -- 'mzero', but decided instead to use Monad, with 'fail'. This is
>> -- more appropriate since we won't be using 'mplus'. See 'liftMaybe'.
>> data TypeableState m a = forall s0 sN. (Typeable s0, Typeable sN)=>
>>                            TypeableState (s0 -> m (a,sN))
>>
>> -- this is probably one of the more non-sensical attempts I've made at
>> -- this... but I'm not sure:
>> runTypeableState :: (Monad m, Typeable s0, Typeable sN)=> TypeableState m a -> s0 -> m (a,sN)
>> runTypeableState (TypeableState st) s0 = (liftMaybe $ cast s0) >>= st
>>
>> -- copied from Control.Monad.StateT
>> instance (Monad m) => Monad (TypeableState m) where
>>     return a = TypeableState $ \s -> return (a, s)
>>     m >>= k  = TypeableState $ \s -> do
>>         ~(a, s') <- runTypeableState m s
>>         runTypeableState (k a) s'
>>     fail str = TypeableState $ \_ -> fail str
>>
>> -- I imagine using this with 'cast' to thread the type in our monad
>> -- transformer
>> liftMaybe :: (Monad m)=> Maybe a -> m a
>> liftMaybe = maybe (fail "Monadic failure") return
>
> So is this even feasible? Or do I not grok what we can and can't do
> with the Typeable class?
>
> Any thoughts on this are appreciated.
>
> Sincerely,
> Brandon Simmons
> http://coder.bsimmons.name
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>