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

[Dan Licata]

[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