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

[Dan Licata]

On Jul25, Claus Reinke wrote:
> although you could introduce a _convention_ by which all view functions
> are supposed to be exhaustive over their input type, the types themselves
> do not encode or check exhaustiveness. so we're talking about an informal
> promise rather than a formal guarantee.

Oh!  I had assumed that it was already considered rude to expose a
non-exhaustive function to the outside world: As far as I know there's
no way to handle the match error (at least in pure code), such as handle
Match in SML, or your lambda-match stuff on the Haskell' list.  So how
can a client use such a function?  Either he has to do a check first (if
canCallF x then f x else ...) or he has to know for other reasons that
the precondition holds.  In either case, it seems like the right thing
to do is to encode the precondition in the type system (if only using
abstract types, so the implementation of the module is still
unverified).  

> one could turn that promise into a type-checked guarantee by using
> explicit sum types (and thus structural rather than name-based typing),
> but that gets awkward in plain haskell.

I don't think the choice of whether you label your variants with names
or with numbers (in1, in2, in3...) has anything to do with the choice of
whether you require your cases to be exhaustive or not.
 
> i often feel limited by the non-extensible, need-to-be-named sum
> types in haskell, and since i intend to use view patterns to encode
> abstract patterns, within a framework of extensible matching, i
> encoded my patterns in an extensible, open fashion.

And if you're using extensible sums, then there always is an extra case
to consider, since there are always potential future extensions that you
don't know about.  So that's a perfect time to use the Maybes.  But I
still maintain that it's wrong to use the outUnit/outArrow style when
what you are defining is in fact a total function into a closed sum
type, since the type of outUnit/outArrow captures what is going on less
precisely.  (Even though neither type captures what is going on exactly,
since they both admit the possibility of exceptions/non-termination.)

> i just wanted to suggest that it might be possible to get the best of
> both worlds: documentation of exhaustiveness and extensible matches
> (see Tullsen's first-class patterns or my library support and examples
> for lambda-match on the haskell-prime list for more discussion of the
> latter).

The way I'd support documentation of exhaustiveness would be to add a
modality of "pure" (exhaustive, terminating, can't raise an exception,
no unsafePerformIO, ...) code to Haskell.  Then you could document the
fact that a view function is really total in its type.  I'm not quite
sure how this modality would work, though.

-Dan