RFC: user defined toplevel commands

[SkySkimmer]

Introduction

Some things can only be done by a sequence of toplevel commands. For instance, declaring an inductive with n constructors involves 1 constant for the inductive, n constants for the constructors, 1 constant for the induction principle and n constants for the computation rules of the induction principle.
Andromeda wants to be generic enough to avoid having a specific inductive toplevel command, but we should give the user something that can be used to define an inductive in one command. This proposal would make the following AML code define HoTT's paths inductive, with an offscreen inductive AML function (ie fully user defined) (I'm not imagining syntax for parameters for this example so they're done as indices instead).

toplevel (* <- new thing *)
    inductive (* <- a function which checks things like positivity etc then returns something understood by AML *)
        "paths" (* <- the name of the inductive *)
        (forall A : Type, A -> A -> Type) (* <- the type of the inductive *)
        (fun paths => (* <- the constructors can access the inductive *)
            [ "idpath" (forall (A : Type) (a : A), paths A a a) ]) (* <- a list of constructors. paths only has one. *)

The toplevel toplevel command and ML type

There are 2 new predefined types. The first is the type of lazy lists:

mltype llist a =
| lnil
| lcons of a and mlunit -> llist a
end

The second is a type which reifies (most) toplevel commands. For this example we will pretend that it only has the constant command.

mltype toplevel =
| Constant of string and judgment
(* ... TODO *)
end

There is a new toplevel command called toplevel, used as toplevel c where c is a computation of type llist toplevel. It evaluates c to a value in the usual way (with the current top handler etc), then:

• if it gets lnil it is done.
• if it gets lcons order thunk it executes the toplevel command associated with the order, then continues as toplevel thunk () in the updated environment.

For instance, the following declares constants T : Type then x : T:

toplevel
    lcons (Constant "T" Type) (fun _ =>
    lcons (Constant "x" (_constant "T")) (fun _ =>
    lnil))

Maybe some commands should not go in the toplevel ML type. For instance I don't know if declaring ML types through toplevel calls is a good idea.

Desugaring with user toplevel

The desugar and typing phases now need to get information from the runtime phase to continue after a toplevel command. I haven't thought about this beyond noting it needs to be done yet.

New generics

As you can see in the above example we need _constant "T" to access the constant we just declared. This is cheating since _constant does not exist (as a constructor, it exists as a pattern).

Dynamic variables

When declaring an inductive type we want to add the computation rules to the beta hints.
This is the now betas = c toplevel command, which would be reified as Now of dynamic a and a. Problems:

• having the same syntax for accessing the value of a lexical and a dynamic variable means dynamic variables don't have special type. This will probably have to be changed, making them more like references with a builtin type dynamic a, the updaters now [in] and an accessor current x (or some such thing).
• Declaring a new dynamic should definitely remain a toplevel command only as it prevents accessing stale dynamics through closures. If new dynamics can be declared through the toplevel command we would need a way to refer to the newly declared dynamic like with constants. However unlike with constants we can't ML type something like _dynamic "x".
  I'm not sure what the use of declaring new dynamics through toplevel would be. It's certainly not necessary for defining inductive TT types, as opposed to updating dynamics.
• Now of dynamic a and a is not a correct constructor declaration as it's a GADT. How should we deal with this?

Lexical binding and toplevel

The following prints 1 then "2" since closures get the lexical part of the environment (which x belongs to) when constructed, so there's no shadowing or typing issue.

let x = 1
toplevel
    lcons (Let "x" "2") (fun _ =>
    print x; lnil)
do x

Alternate syntax

Instead of using toplevel c to evaluate c and do some commands, we could define new toplevel commands.

It would be like toplevel command args = c, then after this we can evaluate command args at the toplevel.

[SkySkimmer]

I think having a builtin dynamic a is a good idea so I'm going to go do that. The only bikeshedding I can see there is what to call the accessor (I used current above) but that's trivial to change so I'm not waiting.

[andrejbauer]

Yes, eventually we need to address this sort of thing. Another one to address is introduction of new binders, so we can write things like Σ (x:A), B directly.

[andrejbauer]

A more radical solution that may work in the short-term is to allow evaluation of strings, i.e., full reification of source code.

[SkySkimmer]

We would need string manipulation functions in AML to use that.
Also it sounds horrible to use.

[andrejbauer]

Yeah, the next step less horrible than that would expose the abstract syntax. But which one, Input, Dsyntax or Rsyntax? Probably not Rsyntax.

[SkySkimmer]

I'm not sure what the point of that would be.

[andrejbauer]

You could create source code in the form of abstract syntax trees and then have it evaluated. Paired with a bit of support from the parser, this ought to allow flexible syntax extensions.

[SkySkimmer]

Paired with a bit of support from the parser

What might that look like?

[andrejbauer]

I was thinking of MetaOcaml for instance, although that by itself doesn't let us define new syntax. There is also Growing a proof assistant which uses Racket to get new extensions in. I am not sure which way to go here, I'd prefer something that isn't super-complicated, even at the expense of expressivity. As you said at the beginning, the annoying thing would be to write all the constructors and inductions by hand all the time, we need to automate that sort of thing. It doesn't much matter whether the user writes

inductive N : Type where
| Z : N
| S : N -> N

end

or

inductive {name="N"; ty=Type; constructors=[("Z", N), ("S", N -> N)]}