[Haskell-cafe] Re: [Haskell] View patterns in GHC: Request for feedback

[Conor McBride]

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