Rough proposal for types and modules

Skip to first unread message

Raph Levien

Jul 22, 2017, 11:29:10 AM7/22/17
I've been thinking a lot, and think I have a rough design including simple types, and also modules. I'll describe it in terms of the lambda-pi interpretation, partly so I don't need to nail down exact syntax.


Right now, "var" and "term" declarations can only have as their RHS a constant declared in a "kind" command. I'll open that up so they can have arbitrary terms, including type variables. I might have a permission bit on terms, so you can't declare a variable of type "sin pi/4". When writing this, though, it occurred to me that a type of "2+2" is quite sensible in many worlds; it's the disjoint sum of two booleans. The type hierarchy bottoms out in a constant called "Type" or some such.

If you say "var T: Type", then "var x: T", the variable "x" has a polymorphic type. The use of "x" in a proof will then cause the resulting lambda-pi expression to have "Pi T: Type." in its prefix. This is fairly parallel to the way term variables induce pi bindings.

The main use case I have in mind for this is the HOL binding described in the LF paper. Type variables can also appear in terms, so I imagine theorems of the form "|- inhabited T -> E. x x = x" (where x has been declared of type T).

Type checking should basically be Hindley-Milner. Fortunately, that's pretty much what I'm already using for proof checking, so I expect the impact on implementation to be fairly small considering the profound change in power.


A _struct_ becomes a tuple built of dependent pairs (associating to the right), where each element of the tuple has a name. In other words, struct.member "compiles to" a lambda-pi term of the form fst (snd (snd... struct)).

Each member of a struct is an item, which corresponds to a lambda-pi expression of some stripe. The main items I'm thinking about are terms (which can be from term declarations or definitions), theorems, and other structs.

In the language, it's possible to declare a struct type, and also to let-bind a struct to a name, ie "let s = structname { item1: x; item2: y }". Then "s.item1" is the same as "x" (so that unification of the two will succeed).

A _module_ is a function from struct (or possibly a number of structs) to a struct. The struct arg is declared at the top of the module (this is "import" in the Python Ghilbert prototype) and is given a name. In other words, the module is a lambda where the type of the bound variable is a struct.

Elements of a struct can be referenced by ".member" syntax. There will also be some kind of shortcut to elide the "struct." prefix, bringing some or all of its names into the local namespace; this would be equivalent to a series of "let foo =" bindings.

Typically there will be one module per file, but I probably won't enforce that, and will have a mechanism not unlike Rust's, where you can say "mod bar { ... }" inline in a file, or "mod bar;" which will go and find "" in the filesystem.

It will be possible to call a module, ie "let struct2 = bar(struct1)". In lambda-pi terms, only the type is preserved, so definitions exported will not be expanded (to use the definitions, you need definitional theorems of the form |- lhs = rhs in the struct).

I can think of a lot of use cases, including:

* struct1 is minimal axioms, and bar creates definitions and definitional theorems.

* struct1 is axioms and definitions, and bar is a library of theorems.

* The source file is ZFC set theory, and struct1 is a construction of the Peano axioms. Then bar is a library of Peano theorems. [I've given more thought how to do this, and am reasonably confident it can be done practically.]

I know this is just a sketch, probably a lot of things aren't clear from what I've written here, but wanted to at least let people know where my thinking is going. My time off work starts in two weeks, and then I expect to really dig into the concrete language design around it and implementation.

Reply all
Reply to author
0 new messages