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

[Conor McBride]

Me:
 > > In the dependently typed setting, it's often the case that the
 > > "with-scrutinee" is an expression of interest precisely because it
 > > occurs
 > > in the *type* of the function being defined. Correspondingly, an
 > > Epigram implementation should (and the Agda 2 implementation now  
does)
 > > abstract occurrences of the expression from the type.

Dan:
 > Oh, I see: you use 'with' as a heuristic for guessing the motive  
of the
 > inductive family elim.  How do you pick which occurrences of the
 > with-scrutinee to refine, and which to leave as a reference to the
 > original variable?  You don't always want to refine all of them,  
do you?

There are two components to this process, and they're quite separable.
Let's have an example (in fantasy dependent Haskell), for safe lookup.

defined :: Key -> [(Key, Val)] -> Bool
defined k []               = False
defined k ((k', _) : kvs)  = k == k' || defined k kvs

data Check :: Bool -> * where
   OK :: Check True

lookup :: (k :: Key; kvs :: [(Key, Val)]) -> Check (defined k kvs) ->  
Val
lookup k []              !!          -- !! refutes Check False; no rhs
{-before-}
lookup k ((k', v) : kvs) p  with k == k'
{-after-}
lookup k ((k', v) : kvs) OK    | True    = v
lookup k ((k', v) : kvs) p'    | False   = lookup k kvs p'

Left-hand sides must refine a 'problem', initially

   lookup k kvs p  where
     k :: Key; kvs :: [(Key, Value)]; p :: Check (defined k kvs)

Now, {-before-} the with, we have patterns refining the problem

   lookup k ((k', v) : kvs) p  where
     k, k' :: Key
     v :: Val
     kvs :: [(Key, Val)]
     p :: Check (k == k' || defined k kvs)

The job of "with" is only to generate the problem which the lines in its
block must refine. We introduce a new variable, abstracting all
occurrences of the scrutinee. In this case, we get the new problem
{-after-}.

   lookup k ((k', v) : kvs) p | b  where
     k, k' :: Key
     v :: Val
     kvs :: [(Key, Val)]
     b :: Bool
     p :: Check (b || defined k kvs)

All that's happened is the abstraction of (k == k'): no matching, no
mucking about with eliminators and motives. Now, when it comes to
checking the following lines, we're doing the same job to check
dependent patterns (translating to dependent case analysis, with
whatever machinery is necessary) refining the new problem. Now,
once b is matched with True or False, the type of p computes to
something useful.

So there's no real guesswork here. Yes, it's true that the choice
to abstract all occurrences of the scrutinee is arbitrary, but "all
or nothing" are the only options which make sense without a more
explicit mechanism to pick the occurrences you want. Such a
mechanism is readily conceivable: at worst, you just introduce a
helper function with an argument for the value of the scrutinee and
write its type explicitly.

I guess it's a bit weird having more structure to the left-hand
side. The approach here is to allow the shifting of the problem,
rather than to extend the language of patterns. It's a much
better fit to our needs. Would it also suit Haskell?

Cheers

Conor