Finally got a look at the Sublime editor. Looks cool! I suppose a few of
those tricks were using special keyboard macros, though... didn't really
'see' what was happening there. But I had an impression of programming
macros by example, which would be really neat.
Lenses for common structures would be a fun library to write in my tacit
language anyway. I do have an advantage over Haskell, here, in that I'm
actually traversing a heterogeneous type (which may contain rationals and
text values) rather than a homogeneous tree data structure: affine
traversals are easier to enforce (if you operate on them, you must have
left some other type in their place).
One thing I'm curious about is whether the following set of (arrowized)
data plumbing operators is complete (i.e. no need for 'first'):
assocl :: (a * (b * c)) ~ ((a * b) * c)
swap :: (a * b) ~ (b * a)
intro1 :: a ~ (1 * a) -- 1 is unit
elim1 :: (1 * a) ~ a
rot3 :: (a * (b * (c * d))) ~ (c * (a * (b * d)))
I haven't figured out a good way to express the proof. But these have
worked for every pure data-plumbing function I've tried writing (or prodded
Prolog into writing for me). There are advantages of a block-free encoding
for the pure data plumbing... especially in a tacit language which needs to
first load the 'block' into the type.
I suppose a block-free encoding of a tree-zipper, traversals, and lenses
would be a pretty good proof. :)
Thanks for the advice, Michael.
On Thu, Aug 29, 2013 at 10:45 PM, Michael Sloan mgsl...@gmail.com wrote:
Substructural type systems do seem to go hand in hand with the lens
menagerie. Speaking quite informally about quite formal topics:
* Affine types seem to have something to do with traversals, as it
violates traversal laws to visit something multiple times. Of course, this
is unchecked in its usage in Haskell.
* Linear types seem to have something to do with isomorphisms. If you
show that all inputs / output possibilities are handled (like GHC's pattern
match checker), then unless a variable has only one or zero possible
values, it must be used (relevant types). If it's only used once (linear),
and the only functions used are isomorphisms, then you know the whole thing
has to be an isomorphism.
I'm doubting the deepness of this one, because you could certainly
construct a valid isomorphism where values are not used in a linear
fashion. Still, it's nice that there's a large set of things that are
straightforwardly isomorphic.
* Prisms are somewhere between what's called an affine traversal and an
isomorphism. They're functions that can fail in one direction but not the
other. If it's not failing in one direction, then running it in the other
must yield the input. A good example of this is if you have a parser that
preserves all syntax info - locations, comments, whitespace, etc. The
parser could fail, but if it doesn't, then the printer ought to take you
back to the exact input.
Overall, lens seems like an excellent place to draw inspiration for a DSL
that is in some ways very imperative (focused on mutation), while also
playing nicely with the type system and providing nice abstractions for
thinking about the properties of your code.
On Thu, Aug 29, 2013 at 9:42 PM, David Barbour dmbarb...@gmail.comwrote:
Thanks for the refs. I hadn't heard of multi-focus zippers. I'll give
modeling those a try soon. Even if just for curiosity. I've used traversals
but I could certainly use a refresher there.
Lenses might also be worth modeling, if I can do so within the limits of
not knowing which types might be linear. Probably not a problem. :)
On Aug 29, 2013 8:58 PM, Michael Sloan mgsl...@gmail.com wrote:
My current preferred text editor nicely supports multiple cursors:
https://www.youtube.com/watch?v=E9QYlmvRVRQ
It's extremely convenient because it's like having some of the power of
macros without the necessity of premeditation. In a sense, it's the
speculative / live version of macros. Now, sublime's implementation of
this isn't perfect, but it's functional enough to obviate macros for my
text editing needs. My ideal multiple cursors implementation would also
attempt to make all cursors visible by omitting intermediary lines when
necessary. Of course, this won't manage all cases - but it would be very
cool to be able to edit a bunch of files at once, seeing all of the
affected code.
Of course, it's also possible with emacs:
https://github.com/emacsmirror/multiple-cursors
As for tree zippers and multiple selections, it turns out that higher
order (higher derivative) zippers introduce multiple focuses:
http://blog.poucet.org/2007/07/higher-order-zippers/
I tried to build a minimal text editor on this idea, and it got very
clumsy, so I'm not really recommending this approach beyond it being a
curiosity. A single zipper was of course beautiful for text editing, but
when you got into the real world of having selections and
