[Haskell-cafe] Re: [Haskell] View patterns in GHC: Request
for feedback
Conor McBride
ctm at cs.nott.ac.uk
Fri Jul 27 05:35:56 EDT 2007
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
More information about the Haskell-Cafe
mailing list