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

[Brandon Simmons]

On Mon, Dec 6, 2010 at 11:53 PM, Luke Palmer <lrpalmer at gmail.com> wrote:
> 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
>

Thanks a lot, Luke. I'd never run across Data.Dynamic before, but
figured something like this existed. Looks perfect.

Thanks so much,
Brandon


> 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
>>
>