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

[Claus Reinke]

life is funny, isn't it? so many people so eagerly discussing conversion 
between non-monadic and monadic code, yet when we asked for your 
opinions and suggestions on this very topic only a short while ago,
we got a total of 4 (four) replies - all quite useful, mind you, so we were
grateful, but still one wonders.. we might have assumed that not many
people cared after all:

http://www.haskell.org//pipermail/haskell/2005-March/015557.html

shall I assume that all participants in this discussion have joined
the Haskell parade since then, and have proceeded rapidly to the
problems of monadic lifting?-) in which case I'd invite you to have
a look at that survey and the papers mentioned.

> > I thought the easy answer would be to inject non-monadic values into the
> > monad (assuming one already rejiggered things to do automatic lifting).

I'd phrase it slightly differently: what (I think) one wants are implicit coercions 
between monadic and non-monadic types of expressions, where the coercions 
lift non-monadic values into the monad in question, while embedding monadic
computations in the current monad to get a non-monadic result if only that is 
needed (although one might think of the latter as partially lifting the operation 
that needs the non-monadic result).

only I wouldn't want those implicit coercions to be introduced unless
programmers explicitly ask for that (one usually only converts code from
non-monadic to monadic once, and while the details of that step might
be tiresome and in need of tool-support, the step itself should be explicit
- see my comment on (2) below).

> Note that in (a), "pure" values are never used where monads are asked
> for, only the other way around.

that is probably where some would beg to differ - if you lift operations,
why not lift values as well?

> I think that supporting syntax (a) for semantics (b) should be a
> feature because: (1) it is (usually) obvious what (a) means; (2) it
> eliminates the single-use variable 'v' - single-use variables like
> this occur a lot in monadic Haskell code, and I think they make it
> harder to read and write; (3) it would support the math-like syntax
> that I presented in my original message.

(1) "(usually) obvious" is tech-speak for "(perhaps) possible to
    figure out, though probably not uniquely determined"?-)

    when mathematicians abuse notation in the "obvious" way,
    there is usually an assumed context in which the intended 
    abuses are clearly defined (if not, there is another context
    in which the "obvious" things will go unexpectedly awry).

(2) the nice thing about Haskell is that it *distinguishes* between
    monadic and non-monadic computations, and between evaluation
    and execution of monadic computations. if you want everything
    mixed into one soup, ML might be your language of choice
    (http://portal.acm.org/citation.cfm?id=178047 , if I recall correctly?
    see the paper discussed in 
    http://lambda-the-ultimate.org/node/view/552
    for one application that demonstrates the power/danger of such
    implicit monads).

(3) using math-like syntax for lifted expressions is common practice
    in some families of Haskell-DSELs, eg. Conal Elliot's Fran. As John
    pointed out, the predefined class-hierarchy is not really helpful    
    for such endeavours, but if one isn't picky, one may ignore classes
    not used.. the "trick" is to lift even constants, so when you get
    to applications, all components are already lifted, and lifting most 
    arithmetic works out fine (Boolean operations are another matter). 

    note, however, that the resulting language, while looking 
    mathematically pure and permitting concise expression of complex
    circumstances, may not have the reasoning properties you expect..

> It might be hard to modify the type checker to get it to work, but I
> think it is possible, and I see no reason not to be as general as
> possible.

here I'd agree, although in contrast to you, I'd be talking about a
complex refactoring under programmer control, not about an implicitly
invoked collection of coercions. I played with that idea after Martin 
Erwig visited our refactoring project in March, and got to a prototype 
type-coercion inference system for a very simple functional language, 
because I found the situation with various existing and, as Erwig/Ren 
pointed out, apparently unrelated monadification algorithms confusing.

apart from the various styles of monadification, which we'd like 
to permit, and have the programmer select, e.g., by type annotations,
there is the slight problem that there are an unbounded number of 
different monadifications (more if one wants to keep annotations to
a minimum), so one needs a sensible bound (one that does not 
exclude any of the alternatives one might want). one also might 
want to be able to choose between the alternatives (or tune the 
system so that taking the first choice works out ok most of the
time). oh, and it shouldn't be too inefficient, and it is really a pain
to re-implement a type-system just to add a few coercion rules to
it (which is why I haven't extended my mini fpl to Haskell yet..).

in light of this, perhaps some more participants in this discussion
might want to look into contributing their suggestions to our old
survey?

cheers,
claus