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
_______________________________________________
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
