On Jul25, Benjamin Franksen wrote:
Dan Licata wrote:
On Jul25, apfelmus wrote:
The point is to be able to define both zip and pairs with one and the same operator :< .
There's actually a quite simple way of doing this. You make the view type polymorphic, but not in the way you did:
type Queue elt empty :: Queue elt cons :: elt -> Queue elt -> Queue elt
data ViewL elt rec = EmptyL | elt :< rec
view :: Queue elt -> ViewL elt (Queue elt) view2 :: Queue elt -> ViewL elt (ViewL elt (Queue elt))
This is cool! The more so because 'view2' can quite easily be defined in terms of 'view'
view2 q = case view q of EmptyL -> EmptyL x :< q' -> x :< view q'
so it suffices to provide the one-level 'view' as a library function.
Right. The way I usually do it is to define, e.g., viewGen :: (Queue elt -> a) -> Queue elt -> ViewL elt a -- expose one level, applying the input to the subterms And then externally you can define view :: Queue elt -> ViewL elt (Queue elt) view = viewGen id view2 :: Queue elt -> ViewL elt (ViewL elt (Queue elt)) view2 = viewGen view etc.
Does this scale to views containing multiple nestable constructors?
I'm not sure quite what you mean? Multiple datatype constructors, rather than just 2? Certainly. Multiple mutually recursive types? Yes, but you need one parameter to each view type for each type in the loop. The main limitation is that you have to program in a style where you first define the deep view function that you need and then you use it. This is somewhat syntactically inconvenient if you have a lot of "view" idioms that you only use once or twice. Of course, then you can just go back to stringing out the cases. -Dan