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

[Claus Reinke]

Hi Dan,

> No, of course not.  All I meant to say is that sometimes you want a
> total view, and that a total view should be given a type that says as
> much.  The latter says this better than the former.  On the other hand,
> there are lots of circumstances in which you want a partial view, and I
> think the (... -> Maybe _) types for those are perfectly appropriate.

indeed. i was only argueing against the 'wrong', or against the unclear
appeal to the type system (which also appears on the wiki page): 

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.

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.
 
> But by this reasoning, every expression you write should have a Maybe
> type, since there's always the possibility of match failure or
> non-termination.  In Haskell, these effects are always implicit in a
> type, so there's no need to add extra summands to account for them. 
> If you think about the *values* of the returned type, then (1 + Typ *
> Typ) is what you want, not ((1 + 1) + (1 + Typ * Typ)).    

yes, but we were talking about the subset of partiality due to 
failure to accept input, rather than the whole class of partiality
due to failure to produce results. in particular, we were talking 
about a syntactically checkable subset of that: exhaustiveness
means checking for a certain set of abstract or concrete patterns
(a function with exhaustive matching can still be partial in results).

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.

others prefer to keep the closed sum types, just use view patterns
to transform between different concrete views. as Connor said,
they will want to avoid the Maybe of treating individual patterns in
isolation, and instead treat complete sets of patterns all the time.
 
i'm not saying that one is better than the other, i'm saying that i
prefer one of them, and that the appeal to typing is misleading
in the form presented.

> Setting aside the "transparent ordinary patterns" feature, I think this
> is exactly what you get above:
> - the data declaration for TypView corresponds to this "as" declaration

> - the view function of type Typ -> TypView can be analyzed for
> exhaustiveness using GHC's exhaustiveness checker

but note that the type does not encode or guarantee whether or
not such a check has happened, let alone was successful.

> - a run-time match failure of view will be reported as such

the declaration of virtual views as sets of exhaustive abstract patterns
was indeed meant to provide the same documentation as a concrete
view declaration would give.
 
> So I don't think I understand what you're going for here.  Could you
> explain?

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).

claus