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