[Haskell-cafe] Re: [Haskell] View patterns in GHC: Request for
drl at cs.cmu.edu
Wed Jul 25 08:35:33 EDT 2007
[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
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
> in the abstract deconstructor variant, this partiality is explicit in the
> 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
More information about the Haskell-Cafe