joelburget/gist:49f8906471fff1dcab6a

## gistfile1.md

      
    Raw
  

              gistfile1.md
            
          
    Setting the Stage

Starting from a dependently typed functional programming environment, I'll make a simplifying but nontrivial assumption - all program development is expressed as a series of changes. For example, if I start from some program f (x : X)(y : Y) = ?, then change the implementation to g (x : X)(y : Y) = ?, that change is known to the environment as "rename f to g", not "munge a character on line 1".
The entire course of program development, from the empty file, is changes like:

rename Bike to Bicycle
add a parameter to vehicles
define a new data type Airplane

Now the environment has information about the intent of every change. This is a really powerful idea I explored in some detail in a blog post.
Details (Questions)

When you make a change, like "rename Bike to Bicycle", how is that change scoped? I suppose it affects just the places that name is in scope? How does this generalize?
What are the change primitives? Strawman:

rename
changing a type (is this primitive?)
deleting a term
adding a term

But, it seems to me that all of those primitives could be expressed as metaprograms. Perhaps there's just one primitive - metaprogramming (AST transformations). The problem I see with this is that we just gave the environment information about what changes mean, but AST transformations seem rather opaque (IE we gave up the power we just won).
What does this end up looking like?

Our work is expressed as a series of program transformations, like:
define f (x : X)(y : Y) : X
rename f g

Getting fancy

Transformations sometimes cancel. rename f g; rename g f becomes id. So does define f : x -> y -> x; undefine f.
Transformations may also commute. define f : x -> y -> x; rename a b; undefine f commutes -> define f : x -> y -> x; undefine f; rename a b;. I hope you can see where this is going - cancellation and commutation together get us to rename a b;. Program transformation simplification!
Big questions:

when can two transformations commute?
when do they cancel?
what is the simplification algorithm (generalizing this commutation and cancelling simplification)?
is this a nice way to program?

normal program development often involves a lot of noise - renaming, speculative development, etc. does your script become a big mess?
can you edit the script?
how reusable is a script?
the example scripts have a distinctly imperative feel. this makes me uncomfortable...


Updates

Updating programs in this style simplifies use of changing libraries.
We have code using f provided by a library.
f 1 2 3

Now the library updates with this change:
...
rename f g
...

Now we update the library, the environment knows that f changed to g, so it can update our code automatically.
g 1 2 3

Of course, that is as simple as updates get. What happens when the change is nontrivial? A well written update script might have notions like:

f was split into two separate functions, g and h. Uses of f should be replaced by g in this case... and h in all others.
The Foo data type has a new field! Here's what it means (including the default value, etc).

Maybe many (most? all?) updates can be automated. Perhaps human intervention is sometimes necessary.
Diff / Merge

I think this is pretty well covered by that blog post I mentioned, but diffs become self-describing and merges fail much less frequently - only when intentions actually differ (not when two orthogonal changes happen to touch the same term)! Or at least that's the idea.