Cur

The language cur is a dependently-typed language that arbitrary Racket meta-programs can manipulate. The core language of cur is essentially TT. The trusted core provides nothing beyond this language. However, untrusted code provides, via Racket meta-programming, features such as modules, top-level definitions, multi-arity functions, implicit partial application, syntax notations, a tactic DSL, interactive tactics, and a programming language meta-theory DSL. These features run at compile time and generate curnel forms, forms in the core language, which are type-checked before they are run.

Arbitrary racket code can run at phases higher than 0, but racket code at phase 0 is unsupported and should result in a syntax error. The language cur exports everything in racket, racket/syntax, and syntax/parse at phase 1.

The language cur provides reflection features to equip users with the tools necessary to write advanced meta-programs. These features include compile-time functions for type-checking, performing naïve type inference, deciding equivalence between cur terms, expanding macros in cur forms, and evaluating cur forms at compile-time. Programmers can use these reflection feature with little fear, as the resulting curnel forms will always be type-checked prior to running.

The curnel forms are provided by the trusted core of the language. The reflection forms and procedures are provided by mostly untrusted, but privileged, code. These features require knowledge of and manipulation of the language implementation and could not be implemented by a user via a library. Everything else in cur is provided by untrusted user-land code—code that any user (with sufficient meta-programming expertise) could write and ship as a library.

TODO: Some repetition