Inspirations from Racket

Contracts

There are a lot of times where having assert statements is useful for debugging and also documentation, but you don't necessarily want a lot of asserts slowing your performance down all of the time. It would be useful to annotate functions with "contracts", which give pre and post-conditions for the function, and then we can turn them on and off at a module level.

Syntax objects

In racket, macros operate on what are known as "syntax objects", which are more featureful than just s-expressions. Specifically, they contain information about lexical scoping and source locations. This is actually really nice. We could do something like this by making a macro for defining macros, which first parsed the raw Expr into a nicer syntax object, operated on the syntax object, and then transformed the syntax object at end back into an Expr.

Patterns

There is a very general form of patterns in racket macros, where you can, for instance, do something like

((a b) ...) => ((+ 1 a) ... b ...)

and it will magically do the right thing. I think there's a formal way of talking about this, but from the outside at least it seems very magical.

Staged compilation

There is a strict separation between phases of computing in Racket. Code that is generated from a macro run at phase n is evaluated at phase n-1. Phases also have different lexical scopes, so that bindings from an earlier phase don't conflict with bindings at a later phase.

This is somewhat similar to how CompTime.jl works. However, CompTime.jl has the downside that the "macro phase" arguments need to be passed in at the type level.

I wonder if it's possible to make something similar to CompTime.jl, but instead of producing Julia code, we produce GAT expressions/context morphisms. This would make writing functions that produce GAT expressions easier, for instance the function that takes in a Petri net and produces a lens would be just like writing a CompTime function, but where the "runtime level" was a GAT expression instead of a Julia expression.

It should also be possible to write generic structures. For instance, lenses should be defined as

@gat_struct SimpleArena ThCartesianCategory begin
  pos::Ob
  dir::Ob
end

@gat_struct SimpleLens ThCartesianCategory begin
  dom::SimpleArena
  codom::SimpleArena
  expose::Hom(dom.pos, codom.pos)
  update::Hom(product(dom.pos, codom.dir), dom.dir)
end

Then given any model of ThCartesianCategory, we should be able to do lenses. Monoidal and regular composition of lenses should then be defined at the level of cartesian categories, using staged metaprogramming.