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