Skip to content

Instantly share code, notes, and snippets.

@runarorama
Created October 9, 2019 14:58
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save runarorama/9d8d03e9d4d07fac9a3cd54d0b8b6f75 to your computer and use it in GitHub Desktop.
Save runarorama/9d8d03e9d4d07fac9a3cd54d0b8b6f75 to your computer and use it in GitHub Desktop.

# Unison Metaprogramming ## Motivation The type io.Mode is _ _type io.Mode = Read | Write | Append | ReadWrite_ _

It really should be unique. We need to make this update. Now, a lot of programs use the io.Mode type, and we'd like them to use the new type. In order to do this, we have to:

1. Replace the hash of the old type with the new one wherever it appears in types or type annotations. 2. Replace the constructors of the type wherever they appear. 3. Replace patterns matching on the type wherever they appear. 4. Transitively propagate the update. The above changes will generate new types and new terms, and their dependents need to get updated and so on.

## The problem Which constructors are which? We can’t rely on the names Read, Write, etc, or on the order of constructors, because the new type’s constructors may have a different order or different names. And what if someone has renamed the constructors locally in their codebase?

We also can’t just offer the ability to map constructors of one type to the constructors of the other type, since the entire shape of the type may have changed. For example, the old type had a constructor that took a Nat and the new one has a constructor that takes either an Int or a String. So rewriting the program to use the new type may be nontrivial.

## Proposal 1: a specialized metalanguage for rewrite rules The programmer supplies rules of the form pattern |-> expr where expr is a Unison expression involving variables captured in pattern, which matches on Unison expressions.

### Examples The motivating example, or rewriting io.Mode:

_ _io.Mode#oldhash |-> io.Mode_ _io.Mode.Read#oldhash |-> io.Mode.Read_ _io.Mode.Write#oldhash |-> io.Mode.Write_ _io.Mode.Append#oldhash |-> io.Mode.Append_ _io.Mode.ReadWrite#oldhash |-> io.Mode.ReadWrite_ _

More complicated examples:

``` map $f (map $g $xs) |-> map (f . g) xs map $f ($xs ++ $ys) |-> map f xs ++ map f ys

foo $x $y |-> flippedFoo $y $x ```

The code that matches the RHS is replaced with the code on the LHS and then updates are propagated to dependents.

### Implementation effort While seemingly simpler than full macros, this may actually have more moving parts:

* Write a representation of Unison ABTs, in Unison. * Come up with a syntax for the metalanguage. * Write a representation of the metalanguage in Unison. * Write a parser for the metalanguage. * Come up with a runtime/evaluator for the metalanguage.

### Advantages/disadvantages An advantage of some rewrite rule languages (see e.g. Banana Algebra) is that rules can be combined algebraically. This is not universally true about rewrite systems, so if we wanted that property we’d have to be careful to implement a system that provides it.

### Refactoring patterns It’s not immediately clear to me how to refactor programs that use pattern matching, with rewrite rules like this. The trouble is that you often want to replace a concrete representation with an abstract one, replacing functions that pattern match on the concrete representation with functions that abstract over the representation (and therefore don’t use pattern matching).

## Proposal 2: a metalanguage for multi-stage Unison In this proposal, we implement staging and code splicing in Unison.

The idea is that Unison could simply be used as its own metalanguage. A "rewrite rule" is then just a program that pattern matches on some Unison code and outputs Unison code. A function of type Code a -> Code b.

### MetaUnison MetaUnison extends Unison with one type constructor Code, and four new language constructs:

* Quasiquote brackets: .< expr >. quotes the stage-n expression expr and lifts it into stage n+1, delaying its evaluation. If expr has the type t, then .<expr>. has the type Code t. * Splicing: .~ expr inserts the code for the expression expr into the code generated by a quasiquotation. For example let x = .<1 + 2>.; .<.~x + .~x>. generates the code 1 + 2 + 1 + 2. * Evaluation: !.expr turns the expression expr from code to a value, forcing its evaluation. If expr has the type Code t then !.expr has the type t. * Cross-stage persistence: Quasiquoted expressions should be able to refer to variables bound in the enclosing scope. For example let x = 1; .<x + x>. should result in the same code as .<1 + 1>.

### Examples The motivating example:

``` use builtin.io

upgradeIOMode : Code (io.Mode#oldHash) -> Code (io.Mode) upgradeIOMode = everywhere (x -> case x of .<Read#oldhash>. -> .. .<Write#oldhash>. -> .. .<Append#oldhash>. -> .. .<ReadWrite#oldhash>. -> .. ) ```

The syntax for quotation and quasiquotation can be debated. The above syntax is taken from MetaOCaml and has the benefit of being easy to type on a qwerty keyboard.

Flip the arguments of a function:

_ _flipArgs : Code (a -> b -> c) -> Code x -> Code x_ _flipArgs f = everywhere (x ->_ _case x of_ _.<.~f x y>. -> .<.~f .~y .~x>._ _x -> x_ _)_ _

Refactor List to Set:

_ _listToSet : Code a -> Code a_ _listToSet f = everywhere (x ->_ _case x of_ _.<case a of >._ _)_ _

### What’s involved?

* Write a representation of Unison ABTs, in Unison. * Write a code-generator combinator library in Unison. * Modify the parser to include quasiquotation, code splicing, and unquotation, which desugars to calls to the above library.

It turns out that with some minor modification to our type system, we can have typed macros. See “A surprisingly simple implementation of staging” in Oleg’s Tagless-Final Cookbook.

Nifty: staging is considerably simplified by the codebase model. The code in the codebase can be used at all stages, whereas code generated at stage n can only be used at stages n and below. So we don’t have to worry about the “separate compilation problem”.

### Advantages/disadvantages A disatvantage of using macros for refactoring code is that refactorings are not at all composable algebraically. Since a macro can alter the code in virtually any way whatsoever, there’s very little reasoning that can be done about macros and there’s no theory of composition other than ordinary function composition.

If we change a “patch” in UCM to be a set of macros, we lose the property that patches can be trivially merged.

## Proposal 3: simple hash substitution It turns out that a lot of really simple cases can be solved just with hash substitution. The motivating example above is such a case.

Basically exactly as what we have now for terms (with patches), but we relax the restrictions a bit and allow data constructor edits in the patch.

This has the benefit of being really simple to implement, but the drawback is that it does nothing to address the nontrivial cases, which remain very tedious.

### Advantages/Disadvantages While this approach is obviously limited, it does retain the property that patches can be trivially merged.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment