Assignment 1:
Statics and Dynamics, Safety, and Finite Data Types
15-312: Principles of Programming Languages (Fall 2023)
On this assignment, you will implement the statics and dynamics of a simple programming language,
PSF, which has product, sum, and function types. You will also prove that the language is safe,
showing some cases of progress and preservation. Finally, you will explore some curious connections
to algebra and logic.
1 Introduction to PSF
On this assignment, we will be working with PSF1, a programming language with products, sums,
and functions.
Typ τ ::= arr( τ1 ; τ2 ) τ1 → τ2 function
unit unit nullary product
prod( τ1 ; τ2 ) τ1 × τ2 binary product
void void nullary sum
sum( τ1 ; τ2 ) τ1 + τ2 binary sum
Exp e ::= x x variable
λ[ τ1 ](x . e2 ) λ (x : τ1 ) e2 abstraction
ap( e ; e1 ) e( e1 ) application
triv ⟨⟩ nullary tuple
pair( e1 ; e2 ) ⟨e1, e2⟩ binary tuple
pr[ l ]( e ) e · l left projection
pr[ r ]( e ) e · r right projection
absurd[ τ ]( e ) absurd( e ) nullary case analysis
in[ l ][ τ1 ; τ2 ]( e ) l · e left injection
in[ r ][ τ1 ; τ2 ]( e ) r · e right injection
case( e ; x1 . e1 ; x2 . e2 ) case e {l · x1 ↪→ e1 | r · x2 ↪→ e2} binary case analysis
The statics and dynamics of PSF are given in Appendices A and B, respectively.
1Creatively standing for “products, sums, and functions”.
Just like E, we define the static semantics of PSF via judgment Γ ⊢ e : τ , where Γ is the context, e
is an expression, and τ is a type. The rules defining this judgment are given in Appendix A.
2.1 Implementation
On the previous assignment, you implemented an ABT structure for working with α-equivalence
classes of terms. On this and all subsequent assignments, we will provide you with the analogous
structures for the languages we will study, as promised. Importantly, you need only worry about the
signature PSF in lang-psf/psf.abt.sig , not the implementation of structure PSF itself.
Observe that there are two sorts in PSF, Typ and Exp , each with their own sub-structure. As
on the previous assignment, you will find the “primed” auxiliaries (such as Exp.Pair’ ) useful for
constructing elements of Exp.t and Exp.out : view -> exp useful for going by cases on an
element of Exp.t .
In this section, we’ll implement the statics; in other words, we’ll write a typechecker.
2.1.1 core/ Utilities
Before we get to implementing, we’ll introduce some common signatures that will be used through-
out the semester.
We’ll often use signature SHOW , denoting a type that can be converted to a string:
core/common/show.sig
1 signature SHOW =
4 val toString: t -> string
The toString function will be used to provide a convenient REPL interface.
Now, we will consider the signature for implementing the statics of a programming language.
First, consider signature CONTEXT , given in Fig. 2.1. In general, there are relatively few require-
ments on a context: there should be an empty context and the ability to append two contexts.
In PSF (and in many languages we’ll work with), though, we will desire additional operations.
This is expressed in signature CONTEXT_PSF in Fig. 2.2: after including all operations from
CONTEXT , we add the ability to insert a variable of a particular type and lookup the type of
a variable.
We provide a structure ContextPSF :> CONTEXT_PSF in lang-psf/context-psf.sml , imple-
mented as a dictionary.
core/statics/context.sig
1 signature CONTEXT =
3 type context
4 type t = context
7 val empty: context
8 val append: context * context -> context
core/statics/statics.sig
1 signature STATICS =
3 structure Typ: SHOW (* parameter *)
4 structure Term: SHOW (* parameter *)
6 structure Context: CONTEXT (* parameter *)
8 structure Error: SHOW (* abstract *)
9 exception TypeError of Error.t
16 val inferType: Context.t -> Term.t -> Typ.t
23 and checkType: Context.t -> Term.t -> Typ.t -> unit
Figure 2.1: The STATICS signature.
lang-psf/context-psf.sig
1 signature CONTEXT_PSF =
3 include CONTEXT
5 type var = PSF.Exp.Var.t
6 type typ = PSF.Typ.t
8 val singleton: var -> typ -> context
9 val insert: context -> var -> typ -> context
11 val lookup: context -> var -> typ
Figure 2.2: The CONTEXT_PSF signature, extending the CONTEXT signature from Fig. 2.1.
Now, consider signature STATICS , also defined in Fig. 2.1. Observe that structures Typ , Term ,
and Context are marked as “parameters”. For example, the typechecker for PSF will ascribe to
the following signature:
lang-psf/statics-psf.sml
1 structure StaticsPSF :>
3 where type Typ.t = PSF.Typ.t
4 and type Term.t = PSF.Exp.t
5 and Context = ContextPSF
On the other hand, the type Error.t is left abstract. We will not grade the quality of your error
messages; thus, throughout the semester, you may choose any type you wish for Error.t ! Here
are some common choices:
• structure UnitError , defined in core/common/error-unit.sml .
It sets type t = unit , allowing you to raise TypeError () . This is is easy to use, but
it may make debugging type errors more challenging.
• structure StringError , defined in core/common/error-string.sml .
It sets type t = string , allowing you to raise TypeError “error message” . This is
fairly easy to use and quite flexible, but it forces you to do string processing in-line.
• structure StaticsErrorPSF , defined in lang-psf/statics-error-psf.sml .
It uses a custom datatype for type t , providing errors for scenarios where an elimination
form is used incorrectly and for when a type assertion fails. This allows you you to factor out
all string processing logic.
• Your own custom implementation, defined directly after structure Error = .
The starter code sets structure Error = StaticsErrorPSF , but you are welcome to change this
as you wish.
Every typechecker should implement:
• inferType , such that inferType context term infers the type of term in context . If
no type exists, it should raise TypeError error , for some error : Error.t .
• checkType , such that checkType context term typ checks that the type of term in
context is typ , returning () . If this is not the case, it should raise TypeError error ,
for some error : Error.t .
Given inferType , it is easy to implement checkType ; we provide its implementation for you. You
may find it productive to use checkType (mutually recursively) from within inferType .
2.1.2 The First of Many
Task 2.1 (40 pts). In lang-psf/statics-psf.sml , implement the statics of PSF given in Ap-
Hint. The rules in Appendix A precisely determine how inferType should behave. If you wish
to determine the type of some expression based on the conclusion of an inference rule, you can
make recursive calls to inferType (and checkType ) to determine (or assert) the types of sub-
expressions as given in the premises.
2.1.3 Testing
See Appendix C; note that for the time being, the dynamics will not be implemented, but your
typechecker will be used to infer the types of expressions in test files and in the REPL.
3 Dynamics
Now that we have determined which programs are well-formed, we will consider how to run these
programs. We give the dynamics of PSF in Appendix B, defined by the judgments e val and
e 7−−→ e′ .
For the dynamics of PSF, we must prove safety, which consists of two properties:
1. Progress, which states that every well-typed program is either a value or can step.
2. Preservation, which states that steps preserve types.
Progress will tell us how to implement the dynamics, and preservation will help us check that the
dynamics are sensible.
3.1 Progress
First, we will prove progress for PSF; then, we will use our proof to implement the language. For
simplicity, you will only focus on the cases for (nullary and binary) sums, void and τ1 + τ2.
Before we can prove the theorem itself, we will need an important lemma.
Lemma 3.1 (Canonical Forms). If e val, then:
1. If · ⊢ e : void, then we have reached a contradiction.
2. If · ⊢ e : τ1 + τ2, then either:
• e = l · e1, for some e1 with e1 val, or
• e = r · e2, for some e2 with e2 val.
Here, we only enumerate the cases for (nullary and binary) sums.
Task 3.1 (10 pts). State the Canonical Forms Lemma for the remaining types in PSF: nullary
products, binary products, and arrow types.
Task 3.2 (10 pts). Prove the cases of Lemma 3.1 for (nullary and binary) sums only.
Hint. In each case, you assume that e val and that e is well-typed. Which assumption should you
go by induction on first?
Hint. Feel free to state that all remaining are vacuous, as long as this claim is true.
Theorem 3.2 (Progress). If e : τ , then either:
• there exists some e′ such that e 7−−→ e′, or
Task 3.3 (25 pts). Prove Theorem 3.2 for the introduction and elimination forms for (nullary and
binary) sums: cases absurd( e ), l · e, r · e, and case e {l · x1 ↪→ e1 | r · x2 ↪→ e2}.
You may omit symmetric cases (e.g., left vs. right branches of a case); simply say “this case
is symmetric”. You can assume that progress is proved for all other forms (i.e., the IH holds).
Moreover, you may use Lemma 3.1, as long as the citations are correct.
3.2 Implementation
Now that we know that every expression form makes progress, we are able to implement PSF!
3.2.1 core/ Utilities
In Section 2.1.1, we discussed core signatures for implementing a statics. Now, we will introduce
the analogous utilities for impementing a dynamics.
First, consider signature STATE , partially reproduced in Fig. 3.1. When implementing dynamics,
we will have two important types: the type of user programs and the type of “machine states”. The
type ’a t in signature STATE represents a machine state, where we will choose ’a to be the
type of programs. We include val initial : ’a -> ’a t to create a machine state containing
a program.
Often, the two machine states will be “taking a step” and “finished with a value”, corresponding to
judgments e 7−−→ e′ and e val. For this purpose, we will extend the signature as shown in Fig. 3.2,
where for PSF, type Value.t will be Exp.t . We provide this structure as StatePSF .
The key signature is signature DYNAMICS , shown in Fig. 3.1. Every dynamics will come equipped
with a state parameter and a term parameter; for example, the dynamics for PSF will ascribe to
the following signature:
lang-psf/dynamics-psf.sml
1 structure DynamicsPSF :>
2 DYNAMICS
3 where State = StatePSF
4 and type term = PSF.Exp.t
Just like with the typechecker, you may choose a suitable structure Error ; the data in a
Malformed exception is for your debugging. We include structure DynamicsErrorPSF in
lang-psf/dynamics-error-psf.sml , although you are welcome to use an error structure de-
scribed in Section 2.1.1.
core/dynamics/state.sig
1 signature STATE =
3 type ’a t
7 val initial: ’a -> ’a t
core/dynamics/dynamics.sig
1 signature DYNAMICS =
3 structure State: STATE (* parameter *)
5 type term (* parameter *)
7 structure Error: SHOW (* abstract *)
8 exception Malformed of Error.t
10 (** `progress term`
12 * Step `term` to a machine state.
13 * If `term` is malformed , raise `Malformed error`, for some `
error : Error.t`.
15 val progress: term -> term State.t
Figure 3.1: The DYNAMICS signature.
core/dynamics/state-transition.fun
1 functor TransitionState(Value: SHOW) :>
3 datatype (’a, ’v) state = Step of ’a | Val of ’v
4 val map2: (’a -> ’b) * (’v -> ’w) -> (’a, ’v) state -> (’b, ’w)
Figure 3.2: The result signature for the TransitionState functor.
Task 3.4 (40 pts). In lang-psf/dynamics-psf.sml , implement the dynamics of PSF given in
Appendix B. You should assume that your input is well-typed.
Hint. The progress theorem precisely determines how progress should be implemented.
• When the proof of progress says that e 7−−→ e′, your code should produce State.Step e’ .
• When the proof of progress says that e val, your code should produce State.Val e .
• When the proof of progress appeals to the IH and cases on the result, you should recursively
call progress and case on State.Step e and State.Val v .
• When the proof of progress uses the Canonical Forms Lemma on e, you should case on
Exp.out e , raising Malformed in cases guaranteed to be impossible.
3.2.2 Testing
See Appendix C; you should be able to replicate the given test outputs. Feel free to build your own
tests (in a test file or in InterpreterPSF.repl () ), as well!
3.3 Preservation
Now, it remains to show that the dynamics for PSF are sensible; i.e., that transitions preserve
Once again, we will first need some lemmas.
Lemma 3.3 (Inversion). The following inversions hold:
1. If Γ ⊢ absurd( e ) : τ , then:
• Γ ⊢ e : void
2. If Γ ⊢ l · e : τ , then:
• τ = τ1 + τ2
• Γ ⊢ e : τ1
3. If Γ ⊢ case e {l · x1 ↪→ e1 | r · x2 ↪→ e2} : τ , then for some τ1, τ2:
• Γ ⊢ e : τ1 + τ2
• Γ, x1 : τ1 ⊢ e1 : τ
• Γ, x2 : τ2 ⊢ e2 : τ
Like Lemma 3.1, we only enumerate the cases for (nullary and binary) sums here.
Task 3.5 (10 pts). Prove the case e {l · x1 ↪→ e1 | r · x2 ↪→ e2} case of Lemma 3.3.
Hint. There is only one possibility to induct on. Furthermore, many cases will be vacuous!
Additionally, we have the following lemma:
Lemma 3.4 (Substitution). If Γ ⊢ e1 : τ1 and Γ, x : τ1 ⊢ e : τ , then Γ ⊢ {e1/x}e : τ .
Now, on to the main theorem:
Theorem 3.5 (Preservation). If e 7−−→ e′, then if · ⊢ e : τ , then · ⊢ e′ : τ .
Task 3.6 (25 pts). Prove Theorem 3.5 for the introduction and elimination forms for (nullary and
binary) sums: cases absurd( e ), l · e, r · e, and case e {l · x1 ↪→ e1 | r · x2 ↪→ e2}.
You may omit symmetric cases (e.g., left vs. right branches of a case); simply say “this case is
symmetric”. You can assume that preservation is proved for all other forms (i.e., the IH holds).
Moreover, you may use Lemmas 3.3 and 3.4, as long as their citations are correct.
4 Computational Trinitarianism
In this section, we will explore how types, algebra, and logic are all fundamentally related.
4.1 Algebra
Consider the types α×β and β×α, for some fixed types α, β. While elements of the former cannot
be used directly in place of elements of the latter, they seem to contain equivalent information. To
prove this, we can exhibit an isomorphism between the types.
Definition 4.1 (Isomorphic Types). An isomorphism between types τ1 and τ2 in PSF consists of
a PSF expression f1 : τ1 → τ2 and a PSF expression f2 : τ2 → τ1 with following two properties.
1. For all values v1 : τ1, we have f2(f1(v1)) = v1.
2. For all values v2 : τ2, we have f1(f2(v2)) = v2.
If there is an isomorphism between τ1 and τ2 in PSF then we say τ1 and τ2 are isomorphic in PSF
and write τ1 ≃ τ2.
Notice that this definition is similar to the notion of “bijection” from set theory.
Note: for simplicity, we will not treat the notion of equality = used in the proofs rigorously, since
it’s beyond the scope of this course. Thus, for our purposes, both proofs need only be argued
informally.
Now, let’s consider a proof that α× β ≃ β × α:
Consider the following functions:
f1 = λ (x : α× β ) ⟨x · r, x · l⟩
f2 = λ (x : β × α ) ⟨x · r, x · l⟩
Clearly, f2(f1(v1)) = v1 for each value v1 : α × β, since the elements of the pair are
swapped and swapped back. The other direction is similar.
This isomorphism serves as a “data migration” scheme: it tells us precisely how to migrate data
stored as α× β to a new format, β × α. Intuitively, this process roughly corresponds to swapping
two columns in a database.
The isomorphism α × β ≃ β × α is an example of a broader pattern: types form an algebraic
structure! Amazingly enough, this isomorphism is much like a fact you learned in elementary
school: a× b = b× a, where a, b ∈ N.
4.1.1 Notation
For the duration of this problem, we will use:
• α, β, γ to represent arbitrary types,
• a, b, c to represent numbers, and
• A , B , C to represent types in the PSF implementation.
Using our implementation of PSF, we can implement type isomorphisms. For example, we imple-
ment the previous isomorphism in lang-psf/tests/iso0.psf .
Task 4.1 (16 pts). Prove each of the following isomorphisms in lang-psf/tests/ , giving two
functions of the appropriate types (first the left-to-right direction, then the right-to-left direction).
In a comment, provide a brief informal justification (1-3 sentences) about why your functions are
mutually inverse. The arithmetic expressions in the “Arithmetic Correspondent” column are just
for reference/intuition.
Type Isomorphism Arithmetic Correspondent File
1. α× unit ≃ α a× 1 = a iso1.psf
2. (α× β)× γ ≃ α× (β × γ) (a× b)× c = a× (b× c) iso2.psf
3. α+ void ≃ α a+ 0 = a iso3.psf
4. α× (β + γ) ≃ (α× β) + (α× γ) a× (b+ c) = (a× b) + (a× c) iso4.psf
5. void → void ≃ unit 00 = 1 iso5.psf
6. α → (β → γ) ≃ (α× β) → γ (cb)a = ca×b iso6.psf
7. α → (β × γ) ≃ (α → β)× (α → γ) (b× c)a = ba × ca iso7.psf
8. (α+ β) → γ ≃ (α → γ)× (β → γ) ca+b = ca × cb iso8.psf
By proving these isomorphisms, you have provided witnesses to the fact that programmers may go
freely between the data representations on each side of the equation. You may even find it useful
to reorganize your data structures with simple arithmetic facts in mind!
There is a remarkable—and influential—correspondence between principles of reasoning (logic)
and principles of programming (type theory) called the propositions-as-types correspondence. In-
formally, the rules of logic determining when a propositional formula φ is a tautology (i.e., always
true) correspond to the typing rules for the corresponding type. In school, the rules of logic are
usually taught in terms of “truth tables” for connectives, defining when propositions are true or
false. And yet when using logic to show that a proposition is true, we give a proof of it. When we
have a proof of φ, the truth table will say that it is always true.
What is a proof, then? The propositions-as-types principle states that a proof of a proposition φ is
a program of the type corresponding to φ (and vice versa), according to the following chart:
Connective Proposition φ Type φ
trivial truth ⊤ unit
conjunction φ1 ∧ φ2 φ1 × φ2
trivial falsehood ⊥ void
disjunction φ1 ∨ φ2 φ1 + φ2
implication φ1 ⊃ φ2 φ1 → φ2
Thus, proving φ1 ⊃ φ2 amounts to writing a program that takes an element of type φ1 (an assumed
proof of φ1) and produces an element of type φ2 (a proof of φ2). This suggests that the proofs
that corresponds to programs are constructive. Indeed, the propositions that we can prove with
programs in PSF correspond to the tautologies of constructive logic. Be careful: we cannot prove
all “classical” tautologies (i.e., tautologies that can be proved via truth tables). All tautologies
that are constructively true also hold classically, but not all tautologies that are true classically
hold constructively.
Let A,B,C be arbitrary propositions, with:
In your solutions, you need not be careful about the fonts; conflate at your convenience.
Example Consider the following formula:
φ ≜ (A ⊃ (A ∨B)) ∧ (B ⊃ (C ⊃ B))
The corresponding type φ is:
( A → A + B )× ( B → ( C → B ))
Thus, we can prove the theorem via the following term:
⟨λ ( a : A ) l · a, λ ( b : B )λ ( c : C ) b⟩
Example Consider the following formula:
φ ≜ (A ∨B) ⊃ A
The corresponding type φ is:
No program of this type exists, since if the input is a right injection, we have no way of transforming
a B into a A .
Task 4.2 (24 pts). In this exercise, you are to explore the propositoins-as-types correspondence
by exhibiting proofs or arguing that none exists. For each proposition φ below, show that φ
is (constructively) true by exhibiting a program e : φ, or argue informally that no such e can
3. (A ⊃ (B ∨ C)) ⊃ ((A ⊃ B) ∨ (A ⊃ C))
4. ((A ⊃ B) ∨ (A ⊃ C)) ⊃ (A ⊃ (B ∨ C))
Define ¬φ ≜ φ ⊃ ⊥.
5. A ⊃ (¬¬A)
6. (¬¬A) ⊃ A
8. ¬¬(A ∨ ¬A)
9. ¬(A ∨B) ⊃ (¬A ∧ ¬B)
10. (¬A ∧ ¬B) ⊃ ¬(A ∨B)
11. ¬(A ∧B) ⊃ (¬A ∨ ¬B)
12. (¬A ∨ ¬B) ⊃ ¬(A ∧B)
Hint. If you believe you have constructed an expression of the correct type, you can check your
solution via InterpreterPSF.repl () . You may also find it helpful to submit your solutions in
a \begin{codeblock} environment, perhaps in PSF concrete syntax (or something close to it).
Remark. A theorem φ is true constructively if there is at least one proof of it. However, it’s
possible for there to be multiple proofs of a given proposition. For example, consider:
Then, φ is unit+ unit, which can be proven via both l · ⟨⟩ and r · ⟨⟩.
Remark. If φ1 ≃ φ2, then φ1 ⊃⊂ φ2. Consider what the type isomorphisms from the previous
question mean logically.
Γ, x : τ ⊢ x : τ
A.1 Functions
Γ, x : τ1 ⊢ e2 : τ2
Γ ⊢ λ[ τ1 ](x . e2 ) : τ1 → τ2
Γ ⊢ e : τ1 → τ2 Γ ⊢ e1 : τ1
Γ ⊢ ap( e ; e1 ) : τ2
A.2 Products
Γ ⊢ triv : unit
Γ ⊢ e1 : τ1 Γ ⊢ e2 : τ2
Γ ⊢ pair( e1 ; e2 ) : τ1 × τ2
Γ ⊢ e : τ1 × τ2
Γ ⊢ pr[ l ]( e ) : τ1
Γ ⊢ e : τ1 × τ2
Γ ⊢ pr[ r ]( e ) : τ2
Γ ⊢ e : void
Γ ⊢ absurd[ τ ]( e ) : τ
Γ ⊢ e : τ1
Γ ⊢ in[ l ][ τ1 ; τ2 ]( e ) : τ1 + τ2
Γ ⊢ e : τ2
Γ ⊢ in[ r ][ τ1 ; τ2 ]( e ) : τ1 + τ2
Γ ⊢ e : τ1 + τ2 Γ, x1 : τ1 ⊢ e1 : τ Γ, x2 : τ2 ⊢ e2 : τ
Γ ⊢ case( e ; x1 . e1 ; x2 . e2 ) : τ
B Dynamics (Eager, Left-to-Right)
B.1 Functions
λ[ τ1 ](x . e2 ) val
ap( e ; e1 ) 7−−→ ap( e′ ; e1 )
e val e1 7−−→ e′1
ap( e ; e1 ) 7−−→ ap( e ; e′1 )
ap( (λ[ τ1 ](x . e2 )) ; e1 ) 7−−→ {e1/x}e2
B.2 Products
e1 7−−→ e′1
pair( e1 ; e2 ) 7−−→ pair( e′1 ; e2 )
e1 val e2 7−−→ e′2
pair( e1 ; e2 ) 7−−→ pair( e1 ; e′2 )
e1 val e2 val
pair( e1 ; e2 ) val
pr[ l ]( e ) 7−−→ pr[ l ]( e′ )
e1 val e2 val
pr[ l ]( pair( e1 ; e2 ) ) 7−−→ e1
pr[ r ]( e ) 7−−→ pr[ r ]( e′ )
e1 val e2 val
pr[ r ]( pair( e1 ; e2 ) ) 7−−→ e2
absurd[ τ ]( e ) 7−−→ absurd[ τ ]( e′ )
in[ l ][ τ1 ; τ2 ]( e ) 7−−→ in[ l ][ τ1 ; τ2 ]( e′ )
in[ l ][ τ1 ; τ2 ]( e ) val
in[ r ][ τ1 ; τ2 ]( e ) 7−−→ in[ r ][ τ1 ; τ2 ]( e′ )
in[ r ][ τ1 ; τ2 ]( e ) val
case( e ; x1 . e1 ; x2 . e2 ) 7−−→ case( e′ ; x1 . e1 ; x2 . e2 )
case( in[ l ][ τ1 ; τ2 ]( e ) ; x1 . e1 ; x2 . e2 ) 7−−→ {e/x1}e1
case( in[ r ][ τ1 ; τ2 ]( e ) ; x1 . e1 ; x2 . e2 ) 7−−→ {e/x2}e2
C PSF Interpreter
We combine StaticsPSF and DynamicsPSF into InterpreterPSF , which ascribes to the follow-
ing signature:
core/interpreter/interpreter.sig
1 signature INTERPRETER =
3 val repl: unit -> unit
4 val evalFile: string -> unit
In lang-psf/tests/ , some small PSF examples are demonstrated in concrete syntax:
lang-psf/tests/tests.psf
1 fn (x : unit) => x;
3 fn (f : unit -> unit + unit) => f <>;
5 <<>, <<>, <>>>;
7 <(fn (x : unit) =>
9 (* boolean negation function *)
10 fn (bool : unit + unit) =>
11 case[unit + unit] bool {
12 | l.x => in[r]{unit , unit}(<>)
13 | r.x => in[l]{unit , unit}(<>)
17 fn (x : unit * void) => case[unit + unit] x.r {};
To run the tests or enter the PSF REPL, change your directory to lang-psf/ and load sources.cm :
smlnj -m sources.cm
– InterpreterPSF.evalFile “tests/tests.psf”;
(Lam (Unit , (x2 . x2)))
Type: (Arrow (Unit , Unit))
Evaluating … val (Lam (Unit , (x8 . x8)))
(Lam ((Arrow (Unit , (Sum (Unit , Unit)))), (f11 . (Ap (f11 ,
Type: (Arrow (( Arrow (Unit , (Sum (Unit , Unit)))), (Sum (Unit ,
Evaluating … val (Lam ((Arrow (Unit , (Sum (Unit , Unit)))), (f17
. (Ap (f17 , Triv)))))
val it = () : unit
– InterpreterPSF.repl ();
-> <<>, in[r]{unit ,unit}(<>) >.r;
(PrR (Pair (Triv , (InR ((Unit , Unit), Triv)))))
Type: (Sum (Unit , Unit))
Evaluating … val (InR ((Unit , Unit), Triv))
Introduction to PSF
Implementation
core/ Utilities
The First of Many
Implementation
core/ Utilities
Preservation
Computational Trinitarianism
Dynamics (Eager, Left-to-Right)
PSF Interpreter