[Haskell-cafe] Re: [Haskell] View patterns in GHC: Request for feedback

[Dan Licata]

On Jul25, apfelmus wrote:
> Dan Licata wrote:
> > There's actually a quite simple way of doing this.  You make the view
> > type polymorphic, but not in the way you did:
> >
> > myzip :: Queue a -> Queue b -> Queue (a,b)
> > myzip a b = case (view a, view b) of
> >               (EmptyL, _) -> empty
> >               (_, EmptyL) -> empty
> >               (h1 :< t1, h2 :< t2) -> (h1,h2) `cons` myzip a b
> >
> > pairs :: Queue a -> Queue (a,a)
> > pairs a = case view2 a of
> >             h1 :< (h2 :< t) -> (h1, h2) `cons` pairs t
> >             _ -> empty
> >
> > The only difference with view patterns is that you can do the view2
> > inside the pattern itself:
> > 
> > pairs (view2 -> h1 :< (h2 :< t)) = (h1,h2) `cons` pairs t
> > pairs _                          = empty
> > 
> > This would be useful if the thing you were viewing were deep inside
> > another pattern.
> 
> Well, the main feature of view patterns is that you can nest them. In
> other words, the canonical way of writing  pairs  would be
> 
>   pairs (view -> h1 :< (view -> h2 :< t)) = (h1,h2) `cons` pairs t
>   pairs _                                 = empty
> 
> Nesting means to decide "later" on how to pattern match the nested part.
> With view2, you have to make this decision before, something I want to
> avoid.
> 
> For example, take the (silly) definition
> 
>   foo :: Queue a -> Queue a
>   foo xs = case view xs of
>      x :< (y :< zs) -> x `cons` zs
>      x :< ys        -> ys
>      EmptyL         -> empty
> 
> Here, ys  is a Queue and  (y :< zs)  is a ViewL. By scrutinizing  xs
> via  view , both have to be a Queue. By scrutinizing it via  view2 ,
> both have to be a ViewL. But I want to mix them.
> 
> The idea is to introduce a new language extension, namely the ability to
> pattern match a polymorphic type. For demonstration, let
> 
>   class ViewInt a where
>     view :: Integer -> a
> 
>   instance ViewInt [Bool] where
>     view n = ... -- binary representation
> 
>   data Nat = Zero | Succ Nat
> 
>   instance ViewInt Nat where
>     view n = ... -- representation as peano number
> 
> be some views of the integers. Now, I'd like to be able to write
> 
>   bar :: (forall a . ViewInt a => a) -> String
>   bar Zero      = ...
>   bar (True:xs) = ...

This doesn't make sense to me:

Zero :: Nat 

and therefore

Zero :: ViewInt Nat => Nat

but you can't generalize from that to 

Zero :: forall a. ViewInt a => a

E.g., Zero does not have type ViewInt [Bool] => Bool


Maybe you wanted an existential instead, and what you're writing is
sugar for

bar :: (exists a . ViewInt a => a) -> String
bar (pack[Nat](view[Nat] -> Zero)) = ...
bar (pack[Bool List](view[Bool List] -> True:xs)) = ...

(where I'm using [] to make the polymorphic instantiations clear).

That is, you open the existential, and then use the view function at the
the unpacked type in each case and match against the result.

Note that matching against types like this is a form of intensional type
analysis.

-Dan