Re: [Haskell] View patterns in GHC: Request for feedback
[I think we should move the rest of this thread to haskell-cafe, since it's getting long. Note that there have already been some responses on both lists.] Hi Claus, On Jul25, Claus Reinke wrote:
I think that the signature
type Typ
unit :: Typ -> Maybe () arrow :: Type -> Maybe (Typ,Typ)
is *wrong* if what you really mean is
type Typ
data TypView = Unit | Arrow Typ Typ view :: Typ -> TypView
different =/= wrong !-)
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.
That is, if what you mean is that every Typ is either Unit or an Arrow *and nothing else* then the latter signature should be preferred, as it makes this fact explicit in the type system.
but that is not what you're saying there at all! you're saying that -within view 'view' of Typ- Typ is mapped to either Unit or Arrow, if the mapping is successfull. there can be other views of Typ,
Right, but the only issue here is whether this particular view function is total or not.
and the types do not guarantee that 'view' itself is exhaustive over Typ (there can be variants of Typ that 'view' fails to map to TypView). in the abstract deconstructor variant, this partiality is explicit in the types, in the concrete view type variant, it is hidden from the types, implicit in the implementation of 'view'.
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)).
btw, it might be useful to permit association of abstract types with abstract deconstructors, so that an extended abstract type (export) declaration somewhat like
type Typ as unit -> () | arrow -> (Typ,Typ)
tells us (and the compiler) that the abstract patterns in the size function are exhaustive (or at least as exhaustive as clients of the abstract type Typ are supposed to be). the proof obligation would be on the exporter of the abstract type, and any pattern match failures relating to this should be reported as view failures.
doing so would declare a virtual view type, similar to the concrete view types used in other examples, so there might be several 'as' clauses for a single abstract type, declaring separate sets of exhaustive abstract deconstructors.
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 - a run-time match failure of view will be reported as such So I don't think I understand what you're going for here. Could you explain? -Dan
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
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
Others have already pointed this out, but it is worth saying again: Maybe is not the only monadic effect which makes sense during pattern-matching. Wolfram Kahl and I have explored some of these things as part of the Pattern Matching Calculus, http://sqrl.mcmaster.ca/~kahl/PMC/ [If you want to jump to the most recent, most complete version, see http://www.cas.mcmaster.ca/~kahl/Publications/TR/Kahl-Carette-Ji-2006b/] Various other monads can be used for pattern-matching-effects. While Maybe is quite classical, List and LogicT give extremely useful alternatives. Jacques
Oh! I had assumed that it was already considered rude to expose a non-exhaustive function to the outside world:
you mean, as in: head, tail, fromJust, ..?-) whether exposing or using those is considered rude or not, the type system has nothing to tell us about their not handling some inputs, and if you get them from precompiled libraries, you don't see the compiler warnings, either.
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 was talking about name-based (as in: this is the sum type named List)
vs structural (as in: this is the sum type build from Cons and Nil) typing.
the former hides (in-)exhaustiveness from the type system, the latter
exposes it.
consider the example code below, where the type system catches the
non-exhaustiveness of g, where the sum structure of its parameter is
exposed, but has nothing to say about f, where the sum structure is
hidden behind a type name.
claus
{-# OPTIONS_GHC -fallow-overlapping-instances #-}
{-# OPTIONS_GHC -fglasgow-exts #-}
{- our own, nameless sum type with injection and unpacking -}
infixr :|
data a :| b
data a :< b = Inj a deriving Show
class Inj a b where { inj :: a -> a: a }
instance Inj a a where { inj a = Inj a ; out (Inj a) = a }
instance Inj a (a:|b) where { inj a = Inj a ; out (Inj a) = a }
instance Inj a b => Inj a (c:|b) where { inj a = Inj a ; out (Inj a) = a }
{- a product type of nested pairs, with selection -}
class Sel a b where sel :: b -> a
instance Sel a a where sel a = a
instance Sel a (a,b) where sel (a,_) = a
instance Sel a b => Sel a (c,b) where sel (_,b) = sel b
{- to match, supply a product of functions covering the sum -}
match :: (Inj x xs, Sel (x->b) fs) => x:
On Jul30, Claus Reinke wrote:
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 was talking about name-based (as in: this is the sum type named List) vs structural (as in: this is the sum type build from Cons and Nil) typing. the former hides (in-)exhaustiveness from the type system, the latter exposes it.
I don't think the juxtaposition you're setting up here, between "name-based" and "structural", is correct. You could just as well choose the elimination form for "name-based" sum types (i.e., datatypes) to be an exhaustive case analysis. It just happens that Haskell chooses to permit non-exhaustive case expressions. -Dan
participants (3)
-
Claus Reinke -
Dan Licata -
Jacques Carette