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