[Haskell] View patterns in GHC: Request for feedback

[Claus Reinke]

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

> 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, 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'.

> In former signature, it's implicit: you have to say externally that a group 
> of destructors, taken together, define a total view.  When programming 
> with the former signature, you always have an extra case to consider, 
> in which all of the destructors fail.

even with concrete view types, you still have to consider the case that
the mapping into that view type can be partial or non-exhaustive (if you
add a constructor to Typ, but forget to update 'view', the type system
will not complain, and matches over TypView will still be 'exhaustive'..).

> The whole point of sum types is that they tell you exactly what cases
> you have to consider.  There's a big difference between the type A and
> the type A+1, and you should use the type system to track this
> difference (or else you end up wiht things like null pointer exceptions
> in Java).

one should also be careful not to expect more from a type than it
can deliver, and not to use A when dealing with A+1.
 
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.

claus