[augeas-devel] Re: [Interfaces] Draft lense

[Nate Foster]

> That's a very nice idea .. typing wise I assume the result of probe is a
> lens, i.e. probe is a function string -> lens -> lens ?

Exactly. I've found probe most useful for debugging lenses built up
using sequential composition, but as I said it's also handy for
zooming in on a part of a big concatenation, one arm of a union, etc.

Something else we've been working on (but this is a bigger task) is
enhancing the surface language with full-blown dependent and
refinement types. So we write functions like this:

  let f (l1 : lens in S1 <-> V1) (l2 : lens where splittable S1 (ctype
l2)) : lens = ...

The interpreter checks that when you call f, you have to pass it
lenses satisfying the precise conditions in the type. This gives
programmers a way to express the conditions that are actually needed
to typecheck the body of the function (something they have to
calculate manually) which can with error messages since the finger
gets pointed at the actual problem.

Nothing is written down in paper form yet, but the slides from
Benjamin Pierce's MFPS talk from May, "Types considered harmful", has
a few details.

Nate