Specify PTS instances with external DSL

[Toxaris]

Users should be able to specify PTS instances without having to recompile any Haskell code.

The hard part is to invent a syntax to express infinite instances.

[Blaisorblade]

The hard part is to invent a syntax to express infinite instances.

I'm concerned this would block the easy part.
So I'd leave that as separate feature, until we figure out some patterns (unless we want a general-purpose DSL for that as a subset of this external DSL).
If I had to guess, I suspect the most common pattern (or the only one occurring) is a set of infinite universes, I guess for universe polymorphism.

[Toxaris]

Here's my proposal for an external DSL:

formula   ::= "true" | "false" | formula ("&&" | "||") formula | constant ("<" | "<=" | "==" | ">" | ">=") constant 
constant  ::= "Int" | "*" | "**" | ... | integer | variable
statement ::= "axiom" constant ":" constant [ "if" formula ] ";"
           |  "sort" constant [ "if" formula ] ";"
           |  "relation" constant constant constant [ "if" formula ] ";"
language  ::= statement*

For example, we can use this language to specify a finite PTS such as System U directly:

sort *;
sort **;
sort ***;
axiom Int : *;
axiom * : **;
axiom ** : ***;
relation * * *;
relation ** * *;
relation *** * *;
relation ** ** **;
relation *** ** **;

Or we can use formulas to specify an infinite system such as System Fωω:

sort c if c >= *;
axiom c : c + 1;
relation c d d if d >= * && c >= d;

For the semantics, we need to reason about the formulas, which should be possible for such a simple language, shouldn't it?

(As a first step, we could leave out the ["if" formula] part of the statements to implement "the easy part".)

[Blaisorblade]

It doesn't sound so bad, even the easy part.

However, I'd like PTSs (ehm, languages) to be named and exportable (not first-class though). That is, to be able to prepend language systemU = ... to the above.

So that you can write stuff like:

import lambdaCube; //exports fomega
language fomega;

Or does this proposal go into a different kind of complication rat's nest?

I'm just wary of copy-pasting definitions around. In particular, I'd like such a DSL to allow moving the definition of System U^2 from Haskell to our codebase — without pasting the definition of U^2 in each new file ;-).

Other question: if we design a DSL, should we keep ********* as the only concrete syntax for constants, rather than *9? We're discussing how to support Fomegaomega, but a concrete program would get boring quickly if you use any extra level.

For the semantics, we need to reason about the formulas, which should be possible for such a simple language, shouldn't it?

The standard methods are trivial (just need a standard interpreter). But you say "reason": do you mean isSubPTS? That still seems hard if you don't reuse an SMT solver :-). However, that's possible at all, since a < b means ∃ c. a + c = b which is expressible in the decidable Presburger arithmetic. I propose to not implement isSubPTS and leave that as possible future work. BTW, an SMT solver (or some other crazy tool) might be able to decide the other criterion for isSubPTS, the one placing lambda* at the top of the lattice.

(As a first step, we could leave out the ["if" formula] part of the statements to implement "the easy part".)

I'm happy to put off adding a second interpreter :-)

[Toxaris]

I was thinking of having a separate language with the sort, axiom and relation keywords. Maybe with some naming convention like: If you put language foo in a pts file, and foo is not predefined, it looks for a foo.language file in the search path.

[Blaisorblade]

I was thinking of having a separate language with the sort, axiom and relation keywords. Maybe with some naming convention like: If you put language foo in a pts file, and foo is not predefined, it looks for a foo.language file in the search path.

👍, also for the naming convention, and probably for reusing the same search path infrastructure as for modules (we do even have a -i option).

I'm fine with whatever extension, though I'd propose .ptslang (with pts standing for the tool name) because .language is slightly too unspecific.

For me, this is enough design for anybody interested to assign himself to the issue and get started implementing this, if wanted. (I'm not assigning myself, at least not yet).