System I Experimentation Tool

Welcome user@38.103.63.60!

This web application provides a friendly tool for experimenting with System I. System I allows inferring principal typings for pure terms of the lambda-calculus with intersection types for arbitrary finite ranks. It is particularly interesting because it can infer types for terms that cannot be typed in other commonly studied systems, as well as the fact that due to the principal typing property, type inference is compositional. System I was first described in Kfoury and Wells's POPL'99 paper, Principality and decidable type inference for finite-rank intersection types. We are currently in the process of extending System I beyond the pure lambda-calculus in order to smoothly handle important programming language constructs like variants, conditionals, and recursive definitions.

Unfortunately, this tool does not presently work with web browsers, such as Lynx, which do not support the use of <meta http-equiv="refresh">.

Direct bug reports and questions to:

(fn [user, host] => user ^ "@" ^ host) ["compositional-web-bugs", "types.bu.edu"];
Participants
Geoffrey Washburn Software Engineering
Assaf Kfoury Theory Consulting
Joe Wells Theory and Technical Consulting
Sebastien Carlier Software Engineering
Bradley Alan Original Unification Code
Bennett Yates Implementation
Ori Schwartz Implementation
Term

When performing type inference you have three choices. One can choose to select a term out of the following examples (in Standard ML syntax) that produce interesting output:

(* typable at rank 3 *)
(fn x => x) (fn y => y y)
(* typable at rank 3 *)
(fn x => fn y => x y) (fn y => y y)
(* typable at rank 3, untypable in System Fw *)
(fn x => z (x (fn f => fn u => f u)) (x (fn v => fn g => g v))) (fn y => y y y)
(* untypable for all ranks *)
(fn x => x x) (fn x => x x)

Or one may enter a lambda-calculus term for which to infer a principal typing in the text-area below:

Or finally, one may select a local file containing a lambda-calculus term to upload:
File:

Implementation

There are presently three implementations of variations of the System I principal typing inference algorithm.

  • The Alan-Washburn implementation closely matches the algorithm for System I presented in the original POPL99 paper and the presently unpublished corresponding extended technical report.
  • The Yates-Schwartz implementation also closely matches the algorithm for System I presented in the original POPL99 paper.
  • The Carlier implementation follows an inference algorithm suitable for System Iω, an extension of System I with the type constant ω. This system and the algorithm used in this implementation are presented in this ITRS02 paper. Note that this implementation solves constraints lazily, and as such is able to assign types to both strong and weakly normalizable terms.
Which implementation would you like to use?   Alan-Washburn    Yates-Schwartz    Carlier


Unification Options

If a term has a principal typing in System I, the inference engine will find it. However, if a term does not have a typing, the unification algorithm will not terminate. The unification algorithm can be made terminating by restricting the highest rank intersection type that it will attempt to unify. Presently, this is only supported by the Alan-Washburn implementation. If this restriction is set too low, some typable terms may not have a typing inferred for them. However, in the interest of preventing this CGI from using too much of the available system resources, the maximum rank we allow is 8. Regardless, many interesting programs are typable at low ranks. Restrict to rank: 


Input Format

Our lambda-calculus parser is capable of accepting input in several different styles of syntax:

(Standard ML) e::=x | fn x => e | e1 e2 | ( e )
(Haskell) e::=x | \x1…xi -> e | e1 e2 | ( e )
(Scheme) e::=x | (lambda (x) e) | (e1 e2)

Which syntax should be used when parsing terms?   SML Haskell Scheme

Output Format

By default the output includes a fairly lengthy and verbose legend. More advanced users may wish for their output to omit the legend. Include Legend

There are two modes of output, standard which includes only the initial constraints and the final substitution, and tracing provides a trace of the unification process. Standard Tracing

In some examples the types may become very large making the skeletons and derivation difficult to read. One may opt to only apply expansion variable substitutions to the skeletons and derivations displayed in the output, which may make those examples easier to read. Apply Expansions Only

The Alan-Washburn implementation computes composed substitutions using safe composition, while the Yates-Schwartz implementation computes chains of small substitutions. The Carlier implementation works with chains internally, but has an option to compose them (using an algorithm different from safe composition). Compose Substitutions

In the Alan-Washburn implementation, E-path Environments are generated and may optionally be included in the output. Include E-path Environment

The XML output from our inference engines can be rendered using XML Stylesheets into several different file formats, which would you like?

  • PDF Gzipped PostScript PostScript XHTML ASCII Text

    • For these formats, you can choose among the following items to be included in your output:

    Initial Typing JudgementUnification InformationFinal Skeleton or Derivation
    Initial SkeletonFinal Typing Judgement

    Additional options relevant for standard unification output:

    Initial Generated Constraint SetFinal Substitution
    Constraint Set at Failure

    Additional options relevant for tracing unification output:

    Constraint SetsSubstitutions
    Selected SubstitutionsIncremental Skeletons

  • Raw XML

    For XML output, the following options are relevant for tracing unification output:

    Selected SubstitutionsIncremental Skeletons


Generate URL

As this tool provides quite a number of configuration options, and it becomes tiresome to readjust your settings on every visit, we provide the option for you to generate a bookmark-able URL that will preserve the options as they are presently set on this page.