[Haskell-cafe] Re: Making monadic code more concise

[Ling Yang]

Thanks Oleg for the feedback. If I understand right, there is a hard (as in
computability) limit for automatic instancing due to the general requirement of
deriving functions off of the behavior of another.

At this point, I wonder: How good are we at doing this? There's languages that
reside in the more expressive corners of the lambda cube, such as Epigram. Some
of the concepts have been translated to Haskell, such as Djinn. Are only
'trivial' results possible, or that the incomputability problems are just moved
into type space?

In any case, it's a good reason to limit the scope of autolifting.

On Tue, Nov 16, 2010 at 2:49 AM,  <oleg at okmij.org> wrote:
>
> Ling Yang wrote
>> I think a good question as a starting point is whether it's possible
>> to do this 'monadic instance transformation' for any typeclass, and
>> whether or not we were lucky to have been able to instance Num so
>> easily (as Num, Fractional can just be seen as algebras over some base
>> type plus a coercion function, making them unusually easy to lift if
>> most typeclasses actually don't fit this description).
>>
>> In general, what this seems to be is a transformation on functions
>> that also depends explicitly on type signatures. For example in Num:
>
> Things start to break down when we get to the higher order. In the first
> order, it is indeed easy to see that the monadification of the term
>        Int -> Int -> Int
> should/could be
>        m Int -> m Int -> m Int
> Indeed, liftM2 realizes this transformation. But what about
>        (Int -> Int) -> Int
> ?
> Should it be
>        (m Int -> m Int) -> m Int
> ?
> A moment of thought shows that there is no total function of the type
>
>        Monad m => ((Int -> Int) -> Int) -> ((m Int -> m Int) -> m Int)
>
> because there is no way, in general, to get from (m Int -> m Int) to
> the pure function Int->Int. That is, we can't write
>        Monad m => (m Int -> m Int) -> m (Int->Int)
> One may try tabulation (for finite domains)
>
> tf f = do
>       vt <- f (return True)
>       vf <- f (return False)
>       return $ \x -> if x then vt else vf
>
> but that doesn't quite work: what if the resulting function is never
> invoked on the True argument. We have needlessly computed that value,
> vt. Worse, we have incurred the effect of computing vt; that effect
> could be failure. We have needlessly failed.
>
> One can say: we need runnable
>
>> class (Monad m) => Runnable m where
>>         exit : m a -> a
>
> are there many monads that are members of that typeclass? For example,
> Maybe cannot be Runnable; otherwise, what is (exit Nothing)? Any Error
> or MonadPlus monad can't be Runnable.
>