YALCI

Yet Another Lambda Calculus Interpreter.

YALCI is a Haskell implementation of System F with a variety of extensions, type checking and type inference (Algorithms T and W). Initially made as what's described but only for STLC, the Simply Typed Lambda Calculus. Greatly based on Benjamin Pierce's (from the Types and Programming Languages book) STLC with extensions and System F (along with its existential types). Also based on Professor Sandra Alves' description of type inference à la ML (particularly, algorithms T and W).

This was made for a university project under the guidance of Professor Mário Florido.

Instructions

The steps for setting YALCI up are as follows:

cabal build

cabal run

If warnings show up, fix them! In case you're required to install a missing dependency, it can be accomplished by using a command such as:

cabal install --lib <library_name>

The issue is very likely to be a missing dependency so this should suffice. Cabal usually fixes them by itself anyway.

You need cabal and GHC in order to use YALCI, as you may have already noticed.

Once you're running the program, write :? and press enter. It should give you about half the indications you need.

As for the other half, I suggest taking a look at Benjamin Pierce's "Types and Programming Languages" book, most particularly its 11th section (which pertains to Extensions) as well all the way through the 22st and the 24th (which pertain to Polymorphism, including Type Reconstruction, System F and Existential Quantifiers).

Syntax and Semantics

I'm going to show each construct and its meaning in a very informal manner.

Syntax	Semantics	Type
true	true a primitive value	Bool
false	false a primitive value	Bool
if t1 then t2 else t3	if statement both possible outputs must be of the same type and the condition has to be a boolean	Bool where t1 has type Bool and T2 = T3 where type of t2 is T2 and type of t3 is T3
0	0 a primitive value	Nat
succ t	successor of a natural used on naturals otherwise there will be an error	Nat where t has type Nat
pred t	predecessor of a natural used on naturals otherwise there will be an error using it on 0 converts itself into 0	Nat where t has type Nat
iszero t	checks if t is 0 if so then converts into true else false	Bool where t has type Bool
x	variable it can be any alpha-numeric name beginning with a lowercase letter and ending with any number of primes (like myX') this is only meant to have no abstraction in cases where its type is being infered	Type variable t it may have any type, depending on the abstraction
\x:T.t	lambda abstraction/function where x has to have type T (given by the programmer) it will be type checked it's treated as a value	T -> T' where T' is the type of t
_:T.t	wildcard just like an abstraction but the bound variable does not occur in t, so it may be omitted	T -> T' where T' is the type of t
\x.t	lambda calculus abstraction without explicit typing its type will be inferred which means t must include only this abs, app and var constructs	T->T' where T is the inferred type variable of x and T' the inferred type of t
t1 t2	lambda calculus application it requires a space in between first t1 evaluates, then t2 and then the app is evaluated	T where T comes from t1's type: T' -> T, and t2 must have type T'
unit	unit a primitive value	Unit
t1;t2	sequencing where t1 has to have type Unit and it will be thrown away after evaluating	T where T is the type of t2, and t1 must have type Unit
t as T	ascription where T is a type given by the programmer and t's type must match it	T where T is the type of t
let x = t1 in t2	let binding any occurrences of x in t2 are substituted by t1 but only after t1 is evaluated	T where T is the type of t2
{l1=t1, ...,ln=tn}	record, which works like tuples but you can also give them labels for making projections if a label is omitted, it will be as if it were label=n where n is index of the cell where its in	{l1:T1, ..., ln:Tn} where T'i is the type of t'i (product types)
let {l1=p1, ..., ln=pn} = {l1=t1, ..., ln=tn} in t	similar to the let case above but with pattern matching for records the pattern matching (p'i) either contains another record-like pattern or a variable name, and will assign it to it's ith counterpart	T where T is the type of t assuming the types of t1...tn
<l1=t1, ..., ln=tn> as T	variant works similarly to a data from haskell it's used for pattern matching using the case construct <labels are required>	<l1:T1, ..., ln:Tn><>where T has the referred type (sum types)
case (<li=vi> as T) of <lj=xj> -> tj	the case includes a pattern and it will match with the ith, out of all j's which will then produce what's on the right side assuming xj=vi also, each match is separated by a pipe (|)	T where all tj must have the same the type T
fix t	simulates recursion (fixed point)	T where t has type T -> T
letrec x:T1 = t1 in t2	a recursive let binding which indirectly employs the fix construct	T where t2 has type T assuming x has type T1
nil[T]	empty list for elements of type T	T
head[T] t	gets the head of a list of type T	T where t has type T
tail[T] t	gets the tail of a list of type T	List T where t has type T
isnil[T] t	checks if a list of type T is empty	Bool where t has type T
cons[T] t1 t2	a list of type T with t1 as the head and t2 as the tail	List T where t1 has type T and t2 has type List T
\X.t	type abstraction abstracts a type using a type variable it's treated as a value	∀X.T where t has type T and X may occur in T
t[T]	type application allows the type T to replace all occurrences of a certain variable within T this targets type annotations	[X->T]T' where t1 has type ∀X.T'
{*T, t} as {∃X, T'}	packs t this will allow its type to be stay hidden and only be compatible with terms from t	{∃X, T} where T'' is the type of t and T' = [X->T]
let {X, x} = t1 in t2	Unpacks t1 into t2 this allows t1 to be used withint t2 just as explained for the pack construct	T2 where T2 is the type of t2 assuming the existence of X and t1 must have type T1 = {∃X, T1'} and, at last, assuming x has type T1'

Don't forget to take a look at the programs/default_tests.txt file, as it contains examples for all constructs of the language.

Writing a number n is the same as writing succ(succ(...(0)...) (so, n succ's). The parser handles this. If the result of a program is in its entirety a number, then it will be pretty-printed as such, rather than the succession of succ's.

You may write programs directly into the command line, as long as they neither follow nor are followed by anything else. Press enter and YALCI will echo its interpretation of the program, its type and its normal form (what it evaluates to, after being evaluated as much as possible).

There are a couple of synonyms for the Lambda Symbol, the Arrow Symbol, the Universal Quantifier Symbol and the Existential Quantifier Symbol:

• Lambda Symbol: , λ, Λ, lambda;
• Arrow Symbol: ->, →;
• Universal Quantifier Symbol: All, forall, ∀;
• Existential Quantifier Symbol: Some, forsome, ∃.

The existential types and packing/unpacking operations allow functional style OOP (Object-Oriented Programming) as well as the usage of ADT's (Abstract Data Types). Take a look at the Existential Quantifiers section (the 24th) from Pierce's book in case you're curious as to how each of the two can be accomplished.

Types

There are three primitive types: Bool, Nat and Unit. Bool is for booleans, Nat is for natural numbers and Unit is for units (with no real application besides sequencing, as of now). Then there are Type Variables, which are only used for Type Inference; they are displayed as a "t" followed by some number starting from 1. Try writing the term \x.x in the command-line. Another form of type Type Variables is the one used by System F. Check the Syntax and Semantics table for more information.

{l1:T1, ..., ln:Tn} is related to the Product Type, more particularly it regards records.

<l1:T1, ..., ln:Tn> is related to the Sum Type, more particularly it regards variants.

T->T' is the Type Arrow, it comes from abstractions.

List T is the List Type where the elements of a list are all of type T.

∀X.T is the Quantifier Type, which represents a term where its outermost abstraction is a type abstraction. T may contain X's. Comes from type abstractions.

{∃X, T} is the Existential Type, which represents a term where an abstracted X occurs in T. Looking at the type alone can be tricky, so check the table for the Syntax and Semantics. It comes from packs.

X is the Base Type, which must begin with an uppercase letter and may contain in between numbers or letters and end with any number of primes. There's no real use to these other than them serving as a placeholder for Type Abstractions. It comes from unbound type variables.

Notes

Existentials can be encoded within System F alone, but I didn't end up implementing the desugaring for that. I didn't feel like it was worth it, my time is better used elsewhere. Pierce talked about it in his 24th section (it has a rather hint-y designation), so you can see how it's done in there.

The interpreter uses, internally, De Bruijn representation of terms in order to facilitate shifting and substituting operations. Alpha Conversion can be assumed for apparently conflicting substitutions. When printing, if two bound names conflict, the innermost name will be given an extra prime until there are no more conflicts.

Simply Typed Lambda Calculus is rather well-known, but System F tends to stay in the shadows. System F is a far more expressive calculus, known as Polymorphic Lambda Calculus. The idea is that types can be quantified, not just terms. For a good reason, it corresponds to Intuitionist Second Order Logic via the Curry-Howard Isomorphism, and this polymorphism is known as Impredicative Polymorphism. Its inference has been shown to be undecideable for quite a while by Wells [1994]. In any case, it's used implicitly by various compilers, even the most modern ones - which goes to show how impactful System F has been to the world of Programming Languages.

Regarding Type Inference or Type Reconstruction, YALCI includes both Algorithm T and Algorithm W (Hindley-Milner-Damas style). Unfortunately, these algorithms in YALCI only cover the least amount of constructs needed for their basic functioning:

• for T, variables, abstractions and applications;
• for W, variables, abstractions, applications and let-bindings.

Commands

Most of the commands are simple and related in purpose. The table is dense because there are multiple configurations for the same thing. It was not well thought out, but serves its purpose. I hope this was not too much of a hurdle.

Command(s)	Usage	Description
(All commands)	—	Command names (the first token of the command) are not case sensitive.
:var, :v, :assign, :a	:v <var_name>	Assign a written term to <var_name>.
:type, :ty, :t	:t <var_name>	Show the type of the term assigned to <var_name>.
:eval, :ev, :e	:e <var_name>	Fully evaluate the term from <var_name>.
:evaln, :evn, :en	:en <number_of_steps> <var_name>	Evaluate (<number_of_steps>) n-steps the term from <var_name>.
:help, :h, :?	:h	Display information regarding the commands.
:show, :sh, :s	:s <var_name>	Show the term assigned to <var_name>.
:desugar, :desug, :des, :d	:d <var_name1> <var_name2>	Desugar the term from <var_name1> and place it into <var_name2>.
:var, :v, :assign, :a, (+ eval)	:v <var_name1> :ev <var_name2>	Evaluate from the current environment (given <var_name2>) and store into <var_name1>.
:var, :v, :assign, :a, (+ evaln)	:v <var_name1> :evn <number_of_steps> <var_name2>	Evaluate n-steps from the current environment and store into <var_name1>.
:load, :l	:l <file_path>	Load terms from file at <file_path>, assigned as <var_name> := <expression>, and load into the environment.
:v?, :vars	:v?	Show the first page (10 environment variables) if a number is not specified.
:v?, :vars	:v? <number>	Show the 'th page (containing 10 environment variables' names).
:m, :mv, :move	:mv <var_name1> <var_name2>	Store the contents of <var_name2> into <var_name1>.
:q, :quit	:q	Close the REPL.
:te, :tenv, :typeenv	:typeenv	Attempt to type all variables in the environment.
:ee, :eenv, :evalenv	:evalenv	Attempt to evaluate all variables in the environment.
:c, :ce, :cenv, :clear, :clearenv	:c	Clear the environment (no variables accessible until new ones are added).
:de, :denv, :desenv, :desugenv, :desugarenv	:de	Desugar all variables in the environment.
:av?, :allvars	:av?	Show all variables in the environment.
:showenv, :showe, :senv, :se	:se	Show the environment.
:showenv, :showe, :senv, :se	:se <page_number>	Show a specific environment page.
:te, :tenv, :typeenv	:te <page_number>	Type a specific environment page.
:ee, :eenv, :evalenv	:ee <page_number>	Evaluate a specific environment page.
<program>	<program>	Shows, then Types and then Evaluates the given program/term.
(Environment pages)	—	Page numbers start at 1.

To-do

Add comments to the code.

Possibly desugaring for existential-related constructs.

Maybe something else?

Lastly...

Don't forget to report any bugs, mistakes or flaws! Do criticize! Thank you!