On Thu 07 May, [EMAIL PROTECTED] wrote:
>
> Adrian Hey writes:
>
> > Consider the following function..
>
> > demo1 :: (a -> b) -> Either a c -> Either b c
> > demo1 f (Left a) = Left (f a)
> > demo1 _ (Right c) = Right c
>
> > My first question is, can programmers safely assume that the
> > compiler is sufficiently smart to avoid duplicating the expression
> > (Right c) in the event that the second match above succeeds?
>
> > One might reasonably hope that the run time implementation of this
> > function will simply return the functions second argument in this
> > case.
>
> Sadly I don't think one can assume this at all, and for a fairly
> good reason. The argument (Right c :: Either a c) and the result
> (Right c :: Either b c) need not have the same runtime
> representation. In a strict language like ML, for example, we might
> well have
Yes, I suppose I should qualify my remark (about returning the second
argument) by saying that programmer can only rely on this if the
two representations are identical. However, in a lazy language it
seems to me that it is practically certain that (Right c) is always
represented by a tag field and pointer to the expression 'c', but
maybe I'm wrong.
I suppose my original message basically boil down to 2 questions,
one simple, the other contentious.
Simple Question
---------------
Is there anything to be gained by using 'as patterns' (in those circumstances
where the type checker permits), or can the programmer safely assume that a
good compiler will re-use any patterns which also appear in expressions?
Contentious Question
--------------------
Does an expression of form (Right c) always have the same type, regardless
of the type of any associated expressions of form (Left a)?
I think it does.
If this is so then shouldn't the type checker take account of the fact
that after a successful match and the expression is known to be of form
(Right c), then the type of the expression then becomes somewhat less
specific (more polymorphic) than it was before the match occurred.
My argument would go something like this:
1- In Haskell the constructors of algebraic data types are supposed to
behave like any other function when they appear in expressions.
In particular the 'Right' constructor has type..
Right :: b -> Either _ b
2- Referential transparency demands that any expression of form (Right b)
is dependent only on the value of b. Likewise the type of this expression
is only dependent on the type of b..
e = Right b
b :: tb
e :: Either _ tb
To say that in some circumstances an expression of form (e = Right b) might
have type..
e :: Either Int tb (for example)
but at other times might have type..
e :: Either Char tb
seems to me to be highly illogical, downright perverse in fact.
I would say it _always_ has type..
e :: Either _ tb
Now, it may well be true that some implementations might use different
representations for e (= Right c) on different occasions, but if this
is so its the responsibility of the compiler implementer to deal with
this transparently. It doesn't seem reasonable (to me at least) to
introduce nasty language semantics (such as equal values having un-equal
types) for no other reason than to cater for this possibility.
Sorry, I probably haven't expressed my opinion with the precision that
computer scientists normally expect, but I'm sure you get the gist of
my argument.
I'd be really interested in what anybody else thinks about this, because
I'm about to try to implement a polymorphic type checker of my own.
I haven't started designing it yet though. I'm still trying to get my
head round some of the subtleties of type semantics and safe inference
methods.
Regards
--
Adrian Hey
