[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