[Haskell-cafe] Re: [Haskell] View patterns in GHC: Request for
drl at cs.cmu.edu
Thu Jul 26 10:54:05 EDT 2007
> In the dependently typed setting, it's often the case that the
> "with-scrutinee" is an expression of interest precisely because it
> 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. That makes things
> a bit trickier to implement, but it's just the thing you need to replace
> "stuck" computations in types with actual values. The "with" construct
> is what makes it possible to keep all the layers of computation in step.
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?
More information about the Haskell-Cafe