Pure2
This page is about Pure2, an interpreter for finite, functional pure type systems.
Pure2
This page is about Pure2, an interpreter for finite, functional
pure type systems.
Pure2 is a simple interpreter for specifying (finite (finite sort, axiom, and rule sets), functional (singly-sorted)) PTS's and tinkering with them. One can posit inhabitants for particular types, query the interpreter for alpha-equivalence or beta-convertibility of pseudo-terms, define simple abbreviations / macros, normalise and type-check pseudo-terms.
I implemented the language as part of studying for my oral qualifying examination, as a tool for testing out some ideas, to convince myself that I understood several topics, and as a language to use for the presentation at the examination. I despise seeing talks with code in hypothetical languages that's never been run, so I wanted to be sure that everything that I showed was executable (and had been type-checked).
Pure2 is implemented in CamlTrax, my dialect of OCaml, and incorporates code from Braque (my evolving-typed language), LamLang / Morphine (my little System-F-based functional language), and Pure (Pure2's predecessor, which I used for several talks at the PL group). The syntax was modelled after (a subset of) Agda's. Compiling the interpreter will require (at least) the following tools: CamlTrax (preprocessor), DypGen (parser generator), OCamlLex (lexer generator), ExtLib (set of libraries), and FindLib (library). To run the interpreter effectively, it would be helpful to use RLWrap, LEdit, or Emacs.
Pure2 is available in GPL'ed source, and
I've also compiled it for several
platforms. There are some compilation
instructions with the source, but you're
a bit on your own there (although I'll
try to help if you have specific
questions / issues that arise). (I no
longer have access to a PPC OSX machine
with the needed tools to compile, so
this version is not going to be
available any more.) |
Pure2 demonstrates its fancy ASCII logo
and some of its basic functionality:
Defining the sorts, axioms, and rules
for Lambda 2 / System F and defining (as
a macro), type-checking, and normalising
the polymorphic identity function. |
Well, there's really no more information available for the time being, sorry! Please check back soon, though, or e-mail me if you have specific questions.
