[Haskell] Re: Mixing monadic and non-monadic functions

[Cale Gibbard]

On 10/09/05, Frederik Eaton <frederik at a5.repetae.net> wrote:
> These are good arguments, and I think this is a good direction for the
> discussion, should it continue.
> 
> > Despite having a fairly mathematical background, I don't really care
> > for the proposed syntax.
> >
> > myList :: [[Integer]]
> > myList = return [1,2,3,4]
> 
> I'm assuming you mean
> 
> myList :: [[Integer]]
> myList = [1,2,3,4]

No, the confusion is over whether to lift the return, because the
inner and outer monads are the same. It's either return [1,2,3,4] ==
[[1,2,3,4]], or it's liftM return [1,2,3,4] == [[1],[2],[3],[4]]

> 
> > Is myList equal to [[1,2,3,4]] or [[1],[2],[3],[4]]? Either
> > interpretation is possible if there is automatic lifting about. If the
> > lifting only occurs when a type error would otherwise have happened,
> > then there will be cases where genuine type errors are happening and
> > being obscured by automatic lifting.
> 
> Perhaps. The question is whether enough type errors will be left over
> to keep type checking useful. I'm willing to explore the possibility
> that there are. This is not the same as an all-purpose, C++-style
> "cast" operator. It only applies to Monads, and it never makes them
> disappear, it only introduces and propagates them. The effect on the
> type system is thus circumscribed. You can only introduce a Monad in
> "monadic context".
> 
> I think there may be better examples than the one you gave. To me it
> it seems intuitive that myList should be [[1,2,3,4]]. It also seems
> intuitive that this can be turned into a general rule, although I'm
> not accustomed to this sort of reasoning.
> 
> By the way, I'm not entirely confident in the definition of "monadic
> context" that I gave in a message dated "Wed, 7 Sep 2005 23:41:41
> -0700".
> 
> > This basically takes a type error reported at compile time, which, in
> > the case where it would have been solved by lifting, is easily
> > resolved by simply adding a line to a do-block or by using liftM, and
> > turns it into a potential behavioural error which may only be detected
> > at runtime, and whose source in the code may not be so obvious (since
> > the lifting was unintentional in the first place).
> 
> This is true, if you see the two values as essentialy different.
> 
> But if you intended to write [[1,2],[3,4]], and you're complaining
> that the type system would no longer save you from omitting the outer
> and middle brackets by accident, then I would say: but even now it
> doesn't save you from omitting just the middle brackets by accident.
> You still have to watch what you type.

Well, the concern isn't so much for explicit lists as such (as errors
there are quite visible), but when the lists involved are abstract
anyway, perhaps hidden in some chain of compositions.
> 
> And I would say, furthermore, that many of the errors that the type
> system currently catches are a result of programs being too far from
> their specifications, in the present syntax, and that if my proposal
> succeeds in bringing them closer, then it isn't clear that there won't
> be a net decrease in errors as a result. Many of the technologies
> which Haskell researchers are inventing to make programming easier
> already have this effect - of making errors harder to detect, but
> compensating by making programs more concise. Strong typing is a great
> language feature, but it isn't the only one.
> 
> > Also, a class instance, say of Num for lists (treating them as
> > polynomials/power series) would suddenly turn one valid piece of code,
> > like [1,2,3] + [4,5,6] defined by automatic lifting, into a completely
> > different one, and suddenly silently introduce bugs into previously
> > written code in the module (perhaps written by another author who had
> > intended to use the automatic lifting).
> 
> Again, I'm trying to imagine a better example. In this case,
> personally: even if I weren't forced to, and even if it just wrapped a
> list, I would create my own polynomial datatype with 'newtype'. Just
> for the sake of clarity. So it would not be a problem. Am I being
> obtuse?
> 

Well, that's true, but many types are instances of Monad and instances
of another class, and often not in a way which is compatible with your
form of lifting. That's the generic version of the point which I'd
hoped would be extracted from the example.

> > ... Automatic lifting is performed in mathematics because it is
> > assumed that the reader is an intelligent human who will be able to
> > infer quite reasonably what is meant in each (often somewhat
> > ambiguous) case. Haskell programs are not written only for humans,
> > but also for the Haskell compiler, which can't be expected to (and
> > quite possibly shouldn't try to) judge the intent of a piece of
> > code.
> 
> This is a most persuasive observation.
> 
> And it is often true that these authors we invoke for mathematicians
> will explicitly "declare" what they mean before adding functions or
> sets, as I am being asked to do. However, they'll also define
> explicitly what a homomorphism is, over and over again, separately;
> for groups, rings, fields, etc.
> 
> But the fact is that we don't really use separate concepts for
> homomorphisms on different categories, when we think about them. And
> if we look closely we can even discover a simple and unambiguous rule
> uniting them, and we can apply this rule to programming language
> design. The fact that the general rule was also given to us in the
> form of different specialized versions, by mathematicians, let alone
> by programmers, doesn't mean that we shouldn't try to do better.
> 
> I think the same is true for a large class of mathematical shorthand
> (and I think that the importance of notation is underrated). I think
> most such shorthand can be understood simply in terms of lifting, and
> I hypothesize that we can find an automatic lifting rule along the
> lines I've described which will not be as ambiguous as you suggest.
> 
Why not look for a way to do the lifting which is explicit, yet not
inconvenient? Monads often do a great job of this on their own. One
can already write code with a fair amount of convenience which works
across monads and which determines its effects based on its inputs.

It may be possible to use template haskell to derive an automatic
monad lifter which could be applied in a controlled fashion, and if
people really like it, it could be given some special syntax perhaps.

Another point which is perhaps important to mention is that the
monadification of some code is not really something which is unique.
The right level of abstraction is sometimes not to just apply liftMn
to everything, but to use something stronger, like MonadPlus, and to
be careful about how everything happens. This can come up when
producing a nondeterministic abstraction of an initially deterministic
algorithm. Full nondeterminism without any optimisation is often not
what you want. You might want to work with a subset of the
combinations of the inputs that may not at first be obvious, and there
are various optimisations which may be necessary to curb combinatorial
explosion (even though laziness often does help a lot here). To do
this sort of optimisation, you need an instance of MonadPlus (or at
least MonadZero, but that's not around anymore). Also, if the whole
thing is autolifted, you can't inject these controls into the middle,
and end up lifting the code by hand anyway. Careful application of the
generic lifting could be very useful, but unrestrained, in many cases
could completely fail to be helpful.

Also, with multiparameter functions, liftMn isn't always the right
thing to apply. Maybe some parameters should be lifted to one monad
and others to another, and the results collected in a suitable
combination. This sort of thing is hard to do automatically, and it
can be difficult to tell.

What we probably want is an explicit, but generic, lifting mechanism,
which takes care of the boilerplate parts of the lifting, but which we
can control with some precision. Doing it automatically everywhere
seems like it could often be inconvenient.

 - Cale