I want to eventually use the modified bidirectional approach used in the paper 'Let Arguments Go First' in Pikelet (see pikelet-lang/pikelet#76). As a stepping stone, it might help to make some simpler examples that closely follow what was shown in the paper in this repository.

Resources

• Let Arguments Go First (paper) (slides)

I think there may be a bug in the handling of nested recursive bindings with embeds... i.e. nested letrecs as in the test I've added here:

curvelogic@39d7c56

(I may be misunderstanding or there may be a way to combine Nest<> or something else to fix this but I'm not seeing it at present.)

When opening the pattern, state depth is not incremented when entering the second scope's pattern so bound variables which actually identify the nested letrec are being looked up in the outer letrec. (Which fails in the test above because there are fewer bindings in the outer letrec than the index of the binding being sought.)

Culprit seems to be a missing .incr() on line 142 of scope.rs. Depth is incremented for unsafe_body but not for unsafe_pattern. I'm not clear in my head yet whether the obvious change of adding the .incr() for the pattern too (like this) is safe or correct but it doesn't seem to break any tests at least.

Users might want to use a string interner for identifiers. We should be able to support this use case.

Initially we have support for locally nameless variable binding, but perhaps it would be handy to also support others, so users could compare them for performance. The original Unbound implementation also supports a nominal representation, for example.

• locally nameless
• nominal
• ordered terms (see freebroccolo's ocaml-ordered-terms implementation)
• scope graphs (see A Theory of Name Resolution)

More variations can be found in steshaw/lennart-lambda.

Unbound has a Rec type for defining recursive patterns. For example:

letrec 
    x = 21 + y
    y = 1
    z = x + y
in
    z + x

Could be described using the following AST:

#[derive(BoundTerm)]
enum Expr {
    Var(Var),
    Literal(i32),
    Add(Box<Expr>, Box<Expr>),
    LetRec(Bind<Rec<Vec<(Name, Embed<Box<Expr>>)>>, Box<Expr>),
}

Lean (apparently) stores the maximum bound variable to improve the performance of its locally nameless representation.

Here is a quote from section 3.3 in Elaboration in Dependent Type Theory (note that 'instantiate/abstract' maps to 'open/close' respectively in our nomenclature):

Although the locally nameless approach greatly simplifies the implementation effort, there is a performance penalty. Given a term t of size n with m binders, it takes O(nm) time to visit t while making sure there are no dangling bound variables. In [21], the authors suggest that this cost can be minimized by generalizing abstract and instantiate to process sequences of free and bound variables. This optimization is particularly effective when visiting terms containing several consecutive binders, such as λx₁ : A₁, λx₂ : A₂, … , λx_n : A_n, t. Nonetheless, we observed that these two operations were still a performance bottleneck for several files in the Lean standard library. We have addressed this problem using a very simple complementary optimization. For each term t, we store a bound B such that all de Bruijn indices occurring in t are in the range [0,B). This bound can easily be computed when we create new terms: the bound for the de Bruijn variable with index n is n + 1, and given terms t and s with bounds Bt and Bs respectively, the bound for the application (t s) is max(Bt,Bs), and the bound for (λx:t,s) is max(Bt,_Bs_−1). We use the bound B to optimize the instantiate operation. The idea is simple: B enables us to decide quickly whether any subterm contains a bound variable being instantiated or not. If it does not, then our instantiate procedure does not even visit the subterm. Similarly, for each term t, we store a bit that is set to “true” if and only if t contains a free variable. We use this bit to optimize the abstract operation, since it enables us to decide quickly whether a subterm contains a free variable.

These optimizations are crucial to our implementation. The Lean standard library currently contains 172 files, and 41,700 lines of Lean code. With the optimizations, the whole library can be compiled in 71.06 seconds using an Intel Core i7 3.6Ghz processor with 32Gb of memory. Without the optimizations, it takes 2,189.97 seconds to compile the same set of files.

Perhaps our Scope<P, T> type could include this binding depth as a field?

cargo-readme seems like a handy tool!

Not sure how best to do this, considering this is a multi-crate repo 🤔

This will be necessary for a 0.1 release of Pikelet.

The paper, The Locally Nameless Representation, has a good section (7.3) on pattern matching. It would be nice to implement this as an example! Unfortunately I can't find any examples of doing this with Unbound.

I'm guessing this would work nicely on the moniker/examples/stlc_data* examples, seeing as we already have records and variants. I'm thinking a pattern syntax like:

+ enum Pattern {
+     Var(FreeVar<String>),
+     Literal(Literal),
+     Ann(Rc<Pattern>, Embed<Rc<Type>>),
+     Record(Vec<(String, Rc<Pattern>)>),
+     Tag(String, Rc<Pattern>),
+ }
+
  #[derive(Debug, Clone, BoundTerm)]
  pub enum Expr {
      /// Annotated expressions
      Ann(Rc<Expr>, Rc<Type>),
      /// Literals
      Literal(Literal),
      /// Variables
      Var(Var<String>),
-     /// Lambda expressions, with an optional type annotation for the parameter
-     Lam(Scope<(FreeVar<String>, Embed<Option<Rc<Type>>>), Rc<Expr>>),
+     /// Lambda expressions
+     Lam(Scope<Rc<Pattern>, Rc<Expr>>),
      /// Function application
      App(Rc<Expr>, Rc<Expr>),
+     /// Case expressions
+     Case(Rc<Expr>, Vec<Scope<Rc<Pattern>, Rc<Expr>>>),
      /// Record values
      Record(Vec<(String, Rc<Expr>)>),
      /// Field projection on records
      Proj(Rc<Expr>, String),
      /// Variant introduction
      Tag(String, Rc<Expr>),
  }

Resources

• The Locally Nameless Representation (Section 7.3)
• Warnings for pattern matching
  • Used in Elm: https://github.com/elm/compiler/blob/fb19899c1d07ea8f772c69a0cd30bf6eb680409a/compiler/src/Nitpick/PatternMatches.hs#L13-L18
  • Used in Rust: https://github.com/rust-lang/rust/blob/57dd722606028cafde656a66edc3206b82cd3bab/src/librustc_mir/hair/pattern/_match.rs#L572-L593

It would be nice to show an example of using Moniker to define Haskell/Idris/Purescript/Agda-style definitions.

• https://www.haskell.org/onlinereport/haskell2010/haskellch4.html
• https://github.com/sweirich/pi-forall/

This should make free-variable calculation and substitutions much quicker.

This is what SimpleFP-v2 uses in its ABT.

Unbound has a Rebind type for defining a series of dependent patterns. For example:

let x = 21
    y = 1 + x
in
    x + y

Could be described using the following AST:

#[derive(BoundTerm)]
enum Expr {
    Var(Var),
    Literal(i32),
    Add(Box<Expr>, Box<Expr>),
    Let(Scope<Rebind<(Name, Embed<Box<Expr>>)>, Box<Expr>),
}

Note that it's probably more idiomatic (in Rust) and cache-friendly to use an underlying Vec inside the Rebind type, rather than using Unbound's linked-list method.

This would be useful for languages where the are multiple namespaces. Examples would be Rust, Haskell, or Elm, where values and types can share names, but point to different things. Eg:

data Foo a = Foo a Int

Foo points to either:

• the type constructor Foo :: Type -> Type
• the value constructor Foo :: forall a . a -> Int -> Foo a

Unbound manages this by adding a phantom type parameter to its Name type. So you could have either Name Type or Name Expr.

We'd like a Subst trait, like in Unbound. It might look something like this:

trait Subst<T> {
    fn subst(&mut self, name: &Name, replacement: &T);
    fn substs(&mut self, replacements: &[(Name, T)]);
}

We should use Rec<P> for this!