Hi Dan On 25 Jul 2007, at 15:18, Dan Licata wrote:
Hi Conor,
[..]
Why are you so fatalistic about "with" in Haskell?
I guess I'm just fatalistic, generally. Plausibility is not something I'm especially talented at.
Is it harder to implement than it looks?
For Haskell, it ought to be very easy.
It seems to be roughly in the same category as our view pattern proposal, in that it's just an addition to the syntax of pattern matching, and it has a straightforward elaboration into the internal language.
Even on the source level, the with-blocks just expand as "helper functions". I wonder if I have the time and energy to knock up a preprocessor...
(Well, for Haskell it's more straightforward than for Epigram, because we don't need to construct the evidence for ruling out contradictory branches, etc., necessary to translate to inductive family elims.)
In the dependently typed setting, it's often the case that the "with-scrutinee" is an expression of interest precisely because it occurs in the *type* of the function being defined. Correspondingly, an Epigram implementation should (and the Agda 2 implementation now does) abstract occurrences of the expression from the type. That makes things a bit trickier to implement, but it's just the thing you need to replace "stuck" computations in types with actual values. The "with" construct is what makes it possible to keep all the layers of computation in step. It's so often exactly the thing you need in dependently typed programming, so maybe that's a point in its favour as a conceivable Haskell feature, given the flow of the type-level computation tide. All the best Conor