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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
