Hello,
Thanks to everybody who replied on this thread. I'm afraid I've got
to go away for a couple of weeks, so I can't join in any more :-(
Here are my views on the most recent postings...
On Mon 11 May, Jon Mountjoy wrote:
----------------------------------
> I would guess 'sometimes'. In some cases of course is it, but in
> other cases you might increase the scope of an expression and thereby
> worsen the space behaviour. Have there been any attempts to
> identify/quantify this?
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 :-)
On Mon 11 May, Olaf Chitil wrote:
---------------------------------
> See my paper:
> Common Subexpressions are Uncommon in Lazy Functional Languages
I think I will to, looks interesting.
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 don't suppose there's any
possibility of expunging them from the language in due course.
No? I thought not.
If I remember right, David Turners Miranda seemed to be able to live without
'as patterns', didn't it?. I never got to use Miranda, I only read about
it.
> 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 :-)
> (I don't know what "_" is) but rather
Just for the record, I use _ as a 'wildcard' instead of a type variable
which occurs only once. Perhaps this is ambiguous wrt quantification?
> Actually, GHC does finally discard type information right at the
> end, so we could do an extra bit of CSE there, but frankly I doubt
> it would buy very much. But I'm willing to stand corrected.
I don't think you can say this. Granted in this trivial example
we are only talking about wasting constructor record per
'demo expression'. But in other more complex examples we could be
talking several. Also the total heap space that gets wasted this way
is not an intrinsic property of the demo function. It depends on
the number of 'demo expressions' (or similar) which get reduced.
I don't think you can predict how many this will be with any generality.
In some programs it could conceivably be huge Nos. Couldn't it?.
It would be nice to re-use the existing constructors, even if the
type checker says thats illegal.
I think its reasonable to assume that this is _operationally_ safe in most
Haskell implementations, even if the Type Checker does reject it.
I imagine that there isn't a single Haskell implemention where the
representation of (Right c) is in any way dependent on the type of the
argument of the 'Left' constructor. Its difficult to see how it can be,
because the type of the 'Left' constructors argument may not be known
at compile time. Also, such dependency implies compliation of numerous
different versions of 'demo' in order to cope with the multitude
of possibilities. If I'm wrong, please correct me. (After all, I've
had nothing to do with any Haskell implementation so it is quite
possible that my assumptions are invalid.)
Also, I note that the problem Jon Mountjoy mentioned is not relevant to
this particular optimisation. This optimisation will have no effect
on the sharing of expressions which are bound to the 'terminal' pattern
variables (Is that correct terminology? Anyway, you know what I mean.)
The only issue is do existing constructor records get re-used, or are new
ones created. I think the first option has to be more efficient, in
both time & space.
> 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'.
I would say that, for all practical purposes, (r == Right c). Its seems
to me that an important feature of Haskell is that constructors are supposed
to behave like functions, are they not? So, given that Right is a (hopefully
well behaved) function, the 'value' of (Right c) is dependent only on the
'value' of c. 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. This smells strongly of 'side effects' to me,
type wise at least.
> 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.
Dr. Kahrs suggestion is perhaps a better formal treatment of this hypothesis.
I'm afraid I couldn't possibly say one way or the other.
On Mon 11 May, S.M.Kahrs wrote:
-------------------------------
> Well, one could argue that the type of r is
> forall a.Either a c
> in which case there is no problem.
> The tricky question is: what exactly is the argument
> that permits us to abstract the type variable a?
> Usually we don't perform any type abstractions during pattern matching.
>
> One could argue that we didn't. All we did was exploiting a type isomorphism:
> the type of Right is
> forall a,b. a->Either b a
> but this is isomorphic (in System F) to
> forall a. a->(forall b.Either b a)
>
> In other words, we would simply allow patterns to have polymorphic types
> and only instantiate the quantifiers if we have to.
> Moreover, when we instantiate polymorphism we could push quantifiers inwards
> (whenever possible) instead of eliminating them.
Thank you very much for this. I have no idea if your correct :-)
I'm afraid I'm just a simple engineer who (like all other engineers)
operates on the basis that if something that works ok (as I believe my
idea does) doesn't gel with current theory then its the theory that needs
'bending'. Unfortunately I don't have the necessary Computer Science
background to do the bending myself.
I suppose the same might also be said of Victor M. Gulias recent suggestion,
but this would perhaps require somewhat more bending.
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.
> 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?
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?
--------------------------
Thanks to everybody who had the patience to read my messages!
Regards
--
Adrian Hey
