On 12-May-1998, Adrian Hey <[EMAIL PROTECTED]> wrote:
> My first reaction to this was to wonder how it could ever be advantageous
> to reduce the same expression several times instead of just once. Then,
> on reflection I thought Gosh!, I see what you mean, thats never occured
> to me before. Lazyness seems so blooming complicated in practice,
> perhaps I'd better revert back to ML :-)
Yes, or of course you could convert to Mercury ;-)
[Sorry, couldn't resist the opportunity for a plug!]
Laziness does seem to cause as many problems as it solves.
> On Mon 11 May, Simon L Peyton Jones wrote:
> ------------------------------------------
> > My advice would be: write clear code, and let the compiler do the
> > CSE.
>
> I take it you mean avoid using 'as patterns'.
I can't speak for SLPJ, of course, but I think not.
"write clear code" means that you should use `as'
patterns iff they make the code clearer.
> > If it doesn't, complain to the compiler writers. You have
> > good reason to believe that it should.
>
> Do you think they will take any notice of me :-)
Yes, I do.
> > Incidentally, I don't think it would be sensible to change
> > the type system to allow the
> >
> > demo1 :: (a -> b) -> Either a c -> Either b c
> > demo1 f (Left a) = Left (f a)
> > demo1 _ r@(Right c) = r
> >
> > What type does r have? Either a c.
>
> I don't think I agree, thats the whole point of my argument.
> Either a c is the type of the second argument of demo1.
> Things are different for 'r' because it it bound to the pattern/expression
> (Right c), so we have more information, and may (subject to
> certain constraints) 'take liberties' with the type assigned to 'r'.
The trouble with this is that you're breaking the whole model on which
the type system is based. One important principle is that the type of
a function argument is always an instance of the corresponding function
parameter type. Another important principle is that a variable has
the same type at every place that it occurs. Now, maybe you can get
away with breaking these sorts of principles, but even if you can get
away with it, I still think it is a hack, and I think it is likely to
bite you one day.
> I would say that, for all practical purposes, (r == Right c)
But this is not the case in Haskell. In Haskell, two expressions that
have the "same" value but different types are *not* the same.
The Haskell type class system means that the types are an important
part of the semantics. (This is a feature, not a bug.)
> Its seems
> to me that an important feature of Haskell is that constructors are supposed
> to behave like functions, are they not?
Yes.
> So, given that Right is a (hopefully
> well behaved) function, the 'value' of (Right c) is dependent only on the
> 'value' of c.
Correct only if you include the type as part of the value.
And note that the type may be implicitly inferred from the context.
> It seems to be absurd to suggest that the type of (Right c) is,
> in some way, also dependent on the type of an expression which is not
> referenced at all.
The type of a polymorphic expression such as `(Right c)' is, as is
always the case in Haskell, determined by the context in which it occurs.
> This smells strongly of 'side effects' to me, type wise at least.
Well, in Haskell two things are true:
- types are automatically inferred from the surrounding context
- types affect the semantics
Toegether, these imply that the semantics of an expression can be
determined by the surrounding context. Thus I suppose you are not
altogether wrong to say that this "smells of 'side effects'".
Nevertheless, I believe that these are the best language design decisions
(and thus we have made the same decisions for the design of Mercury).
Allowing programmers to omit types that can be inferred from the context
makes programs easier to read, IMHO. Allowing the types to affect the
semantics increases expressiveness, and allows programs to be more concise.
This also improves readability, and IMHO these benefits outweigh
the disadvantages of the semantics of untyped expressions sometimes depending
on the context. (Note that this only applies *before* type inference --
after type inference, the semantics of an expression may depend on the
expression's type, but never on on the expression's context.)
> > What type does the result of the fn have? Either b c.
> > Different types. It would be hard (I believe) to specify crisply
> > when it was legitimate for two terms with different types to
> > be as'd together.
>
> On the contrary, I think it should be pretty easy. The pattern (Right c),
> and hence r, should be assigned the same type as the expression (Right c)
> would be assigned if it had been written explicitly (instead of r) on
> the right hand side. If (and ONLY if), having done this, the whole
> function definition is type legal, then we should be ok. If it turns out
> that performing this substitution results is a type error, then we know that
> the 'as pattern' is also invalid.
Not true! Performing the substitution can result in type errors
(unbound type variables) in cases where the 'as pattern' is valid.
> On Mon 11 May, Fergus Henderson wrote:
> --------------------------------------
> > It probably doesn't buy a lot, but IMHO it's easy enough that it's worth
> > doing anyway.
>
> Please excuse my ignorance, I don't know what IMHO means, but I think your
> saying that the optimisation might be handy, even if done in an untyped
> way.
Yes. Actually I was saying that the optimization is easy to do even if
you have a strongly typed intermediate representation.
IMHO stands for "in my humble opinion".
> > I agree, this code should be disallowed.
> >
> > Note that the different types can lead to different semantics.
> > Consider the following code, which is similar to the code above:
> >
> > foo :: (Int -> Float) -> Either Int Char -> Either Float Char
> > foo f (Left a) = Left (f a)
> > foo _ r@(Right c) = classmethod r
> >
> > class Demo t where
> > classmethod :: t -> Either Float Char
> >
> > instance Demo Either Int Char where
> > classmethod = m1
> >
> > instance Demo Either Float Char where
> > classmethod = m2
> >
> > Here `r' has type `Either Int Char', not `Either a Char',
> > and this determines which class method is called.
> > Note that writing
> >
> > foo _ r@(Right c) = classmethod (Right c)
> >
> > would result in compile error (or worse) due to an uninstantiated
> > type variable.
>
> I think in you last code line (above), your doing exactly the substitution
> I suggested earlier, aren't you?
Yes.
> If so, I certainly agree, that if the substituted expression causes any
> kind of type error then the 'as pattern' is invalid.
> Or have I missed the point?
Yes, you missed the point. In my example, the `as pattern' is VALID,
whereas the code that results from substituting out the `as pattern'
in the manner you suggested earlier is invalid.
The reason that the latter code is invalid is that its semantics
are ambiguous -- it's not clear which class method should be called,
since it's not clear which instance of the type class the expression
`(Right c)' belongs to. With the unsubstituted code, the type of `r'
(which in turn is determined by the context(s) in which it occurs,
in particular as the second parameter of the function `foo') is used
to resolve the ambiguity.
Haskell currently allows code such as that in my example,
and I think it should continue to allow it.
If type checkers were to always substitute out `as patterns',
then this example would become illegal, which would be bad, IMHO.
If you want type checkers to substitute out `as patterns' some of
the time but leave them alone at other times, then I would argue
that this is inconsistent and makes things too complex.
--
Fergus Henderson <[EMAIL PROTECTED]> | "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh> | of excellence is a lethal habit"
PGP: finger [EMAIL PROTECTED] | -- the last words of T. S. Garp.
