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

[Frederik Eaton]

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]

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

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?

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

Frederik

> On 09/09/05, Frederik Eaton <frederik at a5.repetae.net> wrote:
> > By the way, I thought it would be obvious, but a lot of people seem to
> > be missing the fact that I'm not (as Sean, I believe, isn't)
> > requesting limited support for 1 or 2 or 3 argument functions or
> > certain type classes to be applied to monads, or for certain
> > operations to defined on certain types. I know at least how to define
> > type classes and functions. If this is what I wanted I would probably
> > do it myself.
> > 
> > > 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 don't know if this is the right way of looking at it. Do you have an
> > example?
> > 
> > My idea is that you should be able to have code like this:
> > 
> > -- (a)
> > 
> > m3 :: a -> m b
> > 
> > m6 = do
> >     m1
> >     m2
> >     m3 (p1 (p2 p3 (p4 m4 p5)) p6)
> >     m5
> > 
> > - where the m* values are functions returning monads and the p* values
> > are so-called "pure" functions, i.e. functions which don't take monad
> > values or return monad results (so currently the above code won't
> > type-check beacuse of m4) - but have it be interpreted as:
> > 
> > -- (b)
> > 
> > m3 :: a -> m b
> > 
> > m6 = do
> >     m1
> >     m2
> >     v <- m4
> >     m3 (p1 (p2 p3 (p4 v p5) p6)
> >     m5
> > 
> > Note that in (a), "pure" values are never used where monads are asked
> > for, only the other way around.
> > 
> > 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.
> > 
> > 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.
> > 
> > Would it mean treating the 'Monad' class specially? Perhaps, but I
> > don't think this is a reason to avoid it. Further, it is likely that
> > whatever is done to extend the type checker could be given a general
> > interface, which Monad would simply take advantage of, using a
> > meta-declaration in the same spirit as "infixr" etc.
> > 
> > Also, I do not think that template haskell is powerful enough to
> > support this, but I'm willing to be proven wrong.
> > 
> > Frederik
> > 
> > --
> > http://ofb.net/~frederik/
> > _______________________________________________
> > Haskell mailing list
> > Haskell at haskell.org
> > http://www.haskell.org/mailman/listinfo/haskell
> >
> 

-- 
http://ofb.net/~frederik/