Propositional Types

A propositional type is a type that is not a traditional datatype but rather asserts some other logical "property" on a term.

Declaring a Propositional Type

type prop List::Sorted(self: List<x>) = ... define what it means for a list to be sorted...;

What is a Corollary?

A corollary is a function that produces only propositional types as a return value. Corollaries are used to enrich existing terms with new type information.

In practice, a corollary is just a function that can be applied with the "fast-forward" inference rule. For example, consider the two functions f and g.

f : A -> B;
g : B -> C;

Here the term f(x) will have the type B. f(x) will not have the type C though, because another function application is necessary to reach C.

However, if g is a corollary you can reach both B and C with a single application. C just "follows" from B. In practice we can't just "fast-forward" through all of these properties because there may be an infinite number of them. This is where proof tactics become important. The programmer can guide the program through the proof with slightly more explicit instructions.

Declaring a Corollary

A corollary definition looks a lot like a normal function definition but with the "prop" marker after "let". Instead of function arguments, a corollary takes a list of dependencies. The return type is the inferred property and the function body is a proof.

let prop assert-is-sorted(self: List<x>): List::Sorted = (
   ... prove that the list is sorted ...
);

What is a quick-prop?

A quick-prop or "Quickly Inferred Propositional Type" is a corollary that will automatically be inferred without intervention from the programmer. Inference of a quick-prop is a constant time operation, so it is inexpensive to apply everywhere.

A quick-prop is declared just like a normal corollary, but with the name "quick-prop".

let prop quick-prop(self: Precondition): InferredProperty = (
   ... proof goes here ...
);

Guarded Quick-Props

Sometimes a quick-prop needs to access adjacent type information to decide if and how it should be applied. Each quick-prop comes with an optional guard which will be unified to filter property inference and obtain new information. A guard can be added to a quick-prop with a second parameter.

let prop quick-prop(self: QuickPropProp, related: ComplicatedDestructuring<x,y>): InferredProperty = (
   ... proof goes here ...
);

Auto Proof Tactics

Rather than drafting statements directly, LSTS @auto(goal) tries to connect a term to a goal using only corollaries. If this is found to be difficult or impossible then auto-proof will just give up.

Auto Proof uses a simple breadth-first search tactic. This tactic complements the punning feature of LSTS to achieve a somewhat customizable search tactic.

good puns = good @auto.

Example: Secondary Data Types

Inside the LM compiler the Type type can have one of three different valid layouts: normal form, denormal form, and super-normal form. Currently this is manually tracked through programmer convention, but ideally this would be tracked with a propositional type.

let find-global-callable(function-name: String, function-type: Type+Into<Type::Normal>): AST;

Here the function signature specifies which layout is expected for the Type parameter. It is even wrapped in an Into type to indicate that arguments should automatically be coerced into this layout.

Type signatures like this have several benefits:

• expectations are made explicit and enforced by the compiler
• coercions are implicit, removing some manual labor for the programmer
• coercions only happen if the type needs to be coerced, the compiler can be smart and avoid duplicate coercions