Assignment 3:
PCF, FPC, and PyCF
15-312: Principles of Programming Languages (Fall 2023)
In this assignment you will explore concepts of self-reference in programming languages. In PCF we
consider self-reference at the term level. Most often students encounter this form of self-reference
when defining recursive functions, those that “call themselves” when applied to an argument. But
self-reference is not inherently tied to functions, and may be usefully isolated using the type self( τ )
of self-referential expressions of type τ . In FPC we consider self-reference at the type level, via
recursive types rec( t . τ ), where t may occur without restriction in τ . Recursive types may be
used to define self-types, which shows that FPC subsumes PCF. Most students are familiar with
recursive types in ML for defining data structures, such as natural numbers and lists, which are
examples of inductive types. These definitions rely on the eager, by-value dynamcis of FPC. When
a lazy, by-name dynamics is used, the “same” recursive types, syntactically, define coinductive
types, namely co-natural numbers and streams. In the first part of this assignment you will explore
these relationships in more detail.
So-called “dynamically typed” languages are promoted as being more powerful and more flexible
than their “statically typed” counterparts: there is no need to please a type checker to get your
code to compile. A commonly-cited example is the ability to form heterogenous lists, those whose
elements are of disparate types, say strings and numbers and booleans all intermixed, with the
implication that this cannot be done in a static language. More generally, advocates of dynamic
language stress the interactive nature of code development in which anything that parses does
something, and one never has to deal with a type checker.
To explore these claims you will implement a dynamic version of PCF, called PyCF, in homage to
a well-known dynamic language. The language is small, though easily extensible, but is faithful to
the core tenets of dynamic typing. As you have learned in class, the irony is that dynamic typing is
but a mode of use of static typing, one in which you confine your attention to a single recursive type.
To substantiate this claim, you will formulate and implement a translation from PyCF into FPC in
which a single recursive type classifies all values of the dynamic language. So-called dynamic types
emerge as a combination of folding in a recursive type and tagging the components of a summand,
leading to considerable run-time overhead. You will consider in detail the translation of a particular
PyCF program to get a better feel for their needless inefficiency.
As Dana Scott said, untyped languages are really uni-typed. And here we ask, just why is that a
good idea?
1 Self-Reference in Expressions and Types
Recall the type self( τ ) of self-referential values of type τ , with introductory form self[ τ ](x . e )
and eliminator form unroll( e ) subject to the dynamics
unroll( self[ τ ](x . e ) ) 7−−→ {self[ τ ](x . e )/x}e
with self[ τ ](x . e ) val. Recall that the type self( τ ) is definable in FPC as the recursive type
rec( t . t → τ ), where t /∈ τ , with self[ τ ](x . e ) being fold( λ (x : self( τ ) ) e ), and unroll( e )
being unfold( e )( e ).
Consider the extension of FPC defined in Appendix B.
Task 1.1 (10 pts).
Assume given a function halve : int → int that computes the floor of half of its argument. Thus,
for example, halve( 3 ) evaluates to 1. You are to define:
1. lg′ : ( int → int ) self, and
2. lg : int → int.
The second, which computes the floor of the binary logarithm of its argument, is to be defined
in terms of the first, an auxiliary function that, on input n computes ⌊lg n⌋.1 Notice that lg′ is
self-referential, and lg is not!
Your solution must be given in terms of the self-types summarized above, within an eager, by-value
interpretation of FPC.
For the next two tasks, define
T ≜ rec t is τ,
τ ≜ E ↪→ unit+ N ↪→ t× bool× t.
The meaning of this type depends on whether FPC is understood eagerly/by-value or lazily/by-
Task 1.2 (20 pts).
For this task assume an eager/by-value dynamics for FPC.
Define the value Emp ≜ fold( E · ⟨⟩ ) of type T , and Node(t1, b, t2) ≜ fold( N · ⟨t1, b, t2⟩ ), a value of
type T when t1 and t2 are values of type T and b is a value of type bool.
In the eager setting this type is inductive in that it is possible to define a recursor for it with the
following statics:
Γ ⊢ e1 : T Γ, x : {ρ/t}τ ⊢ e2 : ρ
Γ ⊢ Trec[ ρ ]( e1 ; x . e2 ) : ρ
1lgn is the base-2 logarithm of n. For simplicity, your implementation may do anything when n ≤ 0.
and the following dynamics:
Trec[ ρ ]( Emp ; x . e2 ) 7−−→ letx be E · ⟨⟩ in e2
r1 = Trec[ ρ ]( t1 ; x . e2 ) r2 = Trec[ ρ ]( t2 ; x . e2 )
Trec[ ρ ]( Node(t1, b, t2) ; x . e2 ) 7−−→ letx be N · ⟨r1, b, r2⟩ in e2
Notice the similarity with the recursor for nat, the difference being that a node has two predecessors
and a label.
Your tasks are as follows:
1. Describe, informally, the values of type T under this interpretation in terms of the above
2. Define, using the recursor, an in-order traversal function
inord : T → bool list.
Feel free to use list operations such as append and cons.
3. Define the recursor in FPC by giving a recursive function R : (T → ρ) self, defined in terms
of x . e2, so that
Trec[ ρ ]( e1 ; x . e2 ) ≜ unroll(R )( e1 ).
Your solution will follow very closely the dynamics, using let to bind the results of the
recursive calls as in the premises of the dynamics rules.
Task 1.3 (20 pts). For this task assume a lazy/by-name dynamics for FPC.
If e is of type T , then the expression unfold( e ) is of type {T/t}τ , the sum type given earlier.
In the lazy setting this type is coinductive in that it is possible to define a generator for it with the
following statics:
Γ ⊢ e1 : σ Γ, x : σ ⊢ e2 : {σ/t}τ
Γ ⊢ Tgen[σ ]( e1 ; x . e2 ) : T
and dynamics:
t1 = Tgen[σ ]( s1 ; x . e2 ) t2 = Tgen[σ ]( s2 ; x . e2 )
unfold( Tgen[σ ]( e1 ; x . e2 ) ) 7−−→ case {e1/x}e2 {E · ↪→ E · ⟨⟩ | N · ⟨s1, b, s2⟩ ↪→ N · ⟨t1, b, t2⟩}
Notice the similarity with the generator for the type conat, the difference being that a node has
two predecessors, and a label.
1. Describe, informally, the values of this type in terms of its unfolding.
2. Define the function
inord : (T → bool stream ) self
that computes an inorder traversal of the given argument of type T . Feel free to use operations
on streams such as append and cons of an element onto a stream. Hint: Your solution will
be very similar to the one given for the inductive case. It will not require the use of the
generator, because it does not compute a value of type T !
3. Define the generator in FPC by giving a recursive function G : (σ → T ) self, defined in
terms of x . e2, so that
Tgen[σ ]( e1 ; x . e2 ) = unroll(G )( e1 ).
Your solution will rely on the lazy/by-name interpretation of FPC, and will follow very closely
the dynamics given above.
2 The Zen of PyCF
In a dynamically typed language, such as Python, Ruby, JavaScript, or Scheme, an implementation
must internally tag values with their class (often called “type”) when they are created, and all
operations must check the class of their operands (perform a “run-time type check”).
In this section, we introduce PyCF, a dynamically-“typed” extension of PCF. For simplicity, we
statically check that closed express do not have unbound variables, but there are no other static
guarantees. The dynamics is more involved because it must impose, check, and remove classes
during execution. Since these checks are baked into the dynamics, they are not visible in the
syntax. Thus, it isn’t possible to program without them!
2.1 Syntax
We summarize the syntax of this language here, writing expressions objects as d instead of e to
distinguish from other languages. Rather than having (static) types, PyCF has (dynamic) classes
which can be checked at run-time.
Sort Abstract form Concrete form
Class c ::= bool bool
Object d ::= x x
bool[ b ] b (True, False)
if( d ; d1 ; d0 ) d1 if d else d0
int[ i ] i (. . . ,−2,−1, 0, 1, 2, . . . )
plus( d1 ; d2 ) d1 + d2 (int addition and list append)
leq( d1 ; d2 ) d1 <= d2
list( d0 ; . . . ; dn−1 ) [d0, . . . , dn−1]
index( d ; dindex ) d[dindex]
len( d ) len(d)
fun( f . x . d ) (see below)
ap( d ; d1 ) d( d1 )
let( d1 ; x . d2 ) (see below)
isinstance[ c ]( d ) isinstance(d, c)
PyCF is an extension of DPCF, adding booleans, integers with primitive addition and less-than-
or-equal-to operations, lists, let bindings, and run-time class checking.
In the concrete syntax, we parse fun( f . x . d ) and let( d1 ; x . d2 ) as declarations to match
familiar programming languages. Programs are lists of declarations, terminated by if __name__
== "__main__": print(d), which gets desugared to a sequence of lets. For example, here is a
program which sums the list [1, 5, 3, 1, 2] :
# Sum a list.
def sum(l):
n = len(l)
def sum_helper(i):
return 0 if n <= i else l[i] + sum_helper(i + 1)
return sum_helper (0)
test = [1, 5, 3, 1, 2]
if __name__ == "__main__":
print(sum(test))
In abstract syntax, this program is is Main, where (up to α-equivalence):
SumHelper ≜ fun(h . i . if( leq(n ; i ) ; int[ 0 ] ; plus( index( l ; i ) ; ap(h ; plus( i ; int[ 1 ] ) ) ) ) )
Sum ≜ fun( sum . l . let( len( l ) ; n . let(SumHelper ; helper . ap(helper ; int[ 0 ] ) ) ) )
Test ≜ list( int[ 1 ], int[ 5 ], int[ 3 ], int[ 1 ], int[ 2 ] )
Main ≜ let(Sum ; sum . let(Test ; test . ap( sum ; test ) ) )
The abstract syntax of PyCF intentionally resembles that of PCF, but without any type informa-
tion.2 But appearances are deceiving! The dynamics of PyCF is radically different from that of
PCF, for reasons that are much deeper than can be explained at the purely syntactic level.
2.2 Dynamics
Because the statics of PyCF is so permissive, the dynamics has to pick up the slack and detect errors
at run-time. Consequently, we need the following set of judgments (defined in Appendix A):
d isnt c d is not of class c
d val d is a closed value
d 7−−→ d′ d steps to d′
d err d incurs a run-time error
Task 2.1 (20 pts). Implement the Index , Fun , Ap , and IsInstance cases of the dynamics of
PyCF in lang-pycf/dynamics-pycf.sml .
Testing As usual, you can test your code using InterpreterPyCF . For example:
2The concrete syntax may resemble3that of another familiar dynamically-“typed” language, as well... 🙂
3Don’t take this too seriously, though - the semantics are sometimes different. For example, there is no mutability
here (variables are true mathematical variables, not assignables), and isinstance(True, int) is false.
- InterpreterPyCF.repl ();
-> 1 + 2 + 3;
(Plus ((Plus ((Int 1), (Int 2))), (Int 3)))
Evaluating … val (Int 6)
-> [1, 2] + [3];
(Plus ((List [(Int 1), (Int 2)]), (List [(Int 3)])))
Evaluating … val (List [(Int 1), (Int 2), (Int 3)])
– InterpreterPyCF.evalFile “tests/triangle.pycf”;
(Let ((Fun (triangle7 . (n8 . (If ((LEq (n8, (Int 0))), (Int 0),
(Plus (n8, (Ap (triangle7 , (Plus (n8, (Int ~1)))))))))))),
(triangle5 . (Ap (triangle5 , (Int 10))))))
Evaluating … val (Int 55)
val it = () : unit
2.3 Dynamic Programming (the other kind)
Now, let’s experiment with programming in PyCF.
Task 2.2 (15 pts). Implement the following operations in PyCF using concrete syntax in lang-pycf/tasks/ .
1. In comprehension.pycf , implement comprehension to satisfy the given specification.
comprehension([f, p, l]) should be analogous to [f(x) for x in l if p(x)] in other
programming languages.
Hint. You may find it useful to draw inspiration from map.pycf and filter.pycf .
2. In sum_default.pycf , implement sum to satisfy the given specification.
In particular, sum should take in “multiple arguments” (really, a list of arguments). You can
assume it will be provided only one or two arguments. The zeroth argument, always present,
will be a list to sum. The first argument, which may or may not be present, will be a value
to start the sum from, defaulting to 0.
This function is similar to sum in Python, which takes in an optional start argument.
3. In matrix_sum.pycf , implement matrix_sum, which sums the elements of a matrix repre-
sented by nested lists.
For example:
• matrix_sum(5) should be 5, since its input is a zero-dimensional matrix (scalar).
• matrix_sum([1, 4, 2]) should be 7, summing the vector as a list.
• matrix_sum([[5, 1], [6, 8]]) should be 20, summing the two-dimensional matrix.
You may assume the input is built only of well-formed matrices; you need not worry about
dimensions. Additionally, you are welcome to copy in functions from the given test files as
you see fit.
To evaluate your file, you can use InterpreterPyCF . In each of the files, there are commented-out
test cases you can uncomment and run. However, when submitting, make sure to comment them
out again!
– InterpreterPyCF.evalFile “tasks/matrix_sum.pycf”;
(Let ((Fun (matrix_sum8 . (m9 . (* your implementation … *)))),
(matrix_sum6 . (Ap (matrix_sum6 , (List [(List [(Int 5), (Int
1)]), (List [(Int 6), (Int 8)])]))))))
Evaluating … val (Int 20)
val it = () : unit
(* remember: comment out test , uncomment `print(matrix_sum)’ *)
3 Compiling PyCF to FPC
The run-time overhead of dynamic typing can be made explicit by translating PyCF into an eager
version of FPC by regarding a PyCF object as an FPC expression with the type dyn, where dyn is
defined as:
dynview[τ ] ≜ (bool ↪→ bool) + (int ↪→ int) + (list ↪→ list( τ )) + (fun ↪→ arr( τ ; τ ))
dyn ≜ rec( d . dynview[d] )
= rec( d . (bool ↪→ bool) + (int ↪→ int) + (list ↪→ list( d )) + (fun ↪→ arr( d ; d )) )
When unfolded, dyn is a sum type whose summands correspond to the classes of PyCF:
dynview[dyn] = (bool ↪→ bool) + (int ↪→ int) + (list ↪→ list( dyn )) + (fun ↪→ arr( dyn ; dyn ))
For brevity, we write τc for the type of the summand with label c:
τbool ≜ bool
τint ≜ int
τlist ≜ list( dyn )
τfun ≜ arr( dyn ; dyn ))
where we define:
bool ≜ (true ↪→ unit) + (false ↪→ unit)
The run-time checks of PyCF amount to case analyses on the class of a value (since dyn is a sum):
if the expected case is encountered, the value is returned, otherwise it results in an error.
3.1 Introduction
Suppose that Γ ⊢ d ok is a well-formed PyCF expression in the PyCF context Γ. You are to
define a translation d by induction on the structure of d that transforms d, a PyCF object, into
an FPC expression that mimics d’s behavior. We require static and dynamic correctness of the
translation.
Theorem 3.1 (Static Correctness). If Γ ⊢ d ok, then Γ ⊢ e : dyn, where Γ = x1 : dyn, . . . , xn : dyn
is the FPC context that corresponds to the PyCF context Γ = x1 ok, . . . , xn ok.
Notice that we assume all variables have type dyn. We must be careful to maintain this invariant
during translation when going under a binder!
The dynamic correctness is more difficult to specify precisely; the tools required are beyond the
scope of this course. However, one may keep in mind the following guidelines for the transla-
1. A PyCF expression is erroneous (incurs a run-time error) iff its translation into FPC produces
a run-time error.
2. A PyCF expression evaluates to a value of class c iff its translation into FPC evaluates to a
value of type dyn of the form fold( c · v ) for a value v : τc.
3. A PyCF expression d should diverge iff its translation e diverges in FPC.
4. The order of evaluation of sub-expressions should be exactly the same under translation as it
is in PyCF.
Now we define the helper expressions for dealing with dynamic class checking and recursive func-
3.2 Tagging and Untagging
We wish to define two derived FPC constructs corresponding to tagging and untagging values
according to their class:
Γ ⊢ e : τc
Γ ⊢ new[ c ]( e ) : dyn
Γ ⊢ e : dyn
Γ ⊢ cast[ c ]( e ) : τc
In these rules, the type τc for class c is determined by the unrolling of the recursive type dyn as
defined before. The purpose of new is to add a class tag to e and, dually, cast removes this class
tag and returns the contained data if the class was correct and produces an error otherwise.
Task 3.1 (10 pts). Define the operation new[ c ]( e ) with the above typing as a derived form in
FPC, using the expression forms given in Appendix B. These operations may be thought of as the
introduction forms for the recursive type dyn representing values of PyCF.
Task 3.2 (10 pts). Define the operation cast[ c ]( e ) with the above typing in FPC, using the
expression forms given in Appendix B. These are the elimination forms for the recursive type
Task 3.3 (10 pts). Implement new[ c ]( e ) and cast[ c ]( e ) in translate/synext.sml . You will
find the functions in translate/synext-helpers.sml helpful.
Hint. You should not case on e, which could be an arbitrary expression of the appropriate type
according to the rules above. In fact, e need not terminate, let alone be a value. Instead, you may
wish to case on c (either explicitly or via auxiliary functions such as classToSummand Dyn ).
3.3 Recursive Functions
To translate recursive functions from PyCF, we will need to recover recursive functions in FPC. In
particular, we want a way to define recursive functions into FPC which admits the following typing
Γ, f : τ1 → τ2, x : τ1 ⊢ e : τ2
Γ ⊢ fun[ τ1 ; τ2 ]( f . x . e ) : τ1 → τ2
Task 3.4 (10 pts). Implement fun[ τ1 ; τ2 ]( f . x . e ) in FPC in translate/synext.sml . This
utility should be generic in FPC, and is not specifically tied up with PyCF and dyn type. You should
make use of self types from translate/synext-helpers.sml , which are defined as follows:
self( τ ) ≜ rec( t . t → τ )
self[ τ ](x . e ) ≜ fold[ t . t → τ ](λ[ self( τ ) ](x . e ) )
unroll( e ) ≜ unfold( e )( e )
Now, we may use recursive functions in our translation, given that they are definable in FPC.
We have to be careful translating recursive functions, since in the FPC definition fun[ τ1 ; τ2 ]( f .
x . e ), variable f has type τ1 → τ2 while x has type τ1. However, in the translation, every variable
must have type dyn.
3.4 Putting it All Together
We can now tackle the actual translation. Using these auxiliary notions, define the translation
function d to satisfy the criteria specified above. To get you started, here are a few cases.
bool[ b ] = new[ bool ]( b )
if( d ; d1 ; d0 ) = if( cast[ bool ]( d ) ; d1 ; d0 )
list( d0 ; . . . ; dn−1 ) = new[ list ]( list( d0 ; . . . ; dn−1 ) )
index( d ; dindex ) = index( cast[ list ]( d ) ; cast[ int ]( dindex ) )
Task 3.5 (40 pts). Using the auxiliary constructs given above, define all the other cases for the
translation d.
Hint. Keep in mind that your translation must satisfy the properties listed above. In particular,
according to Theorem 3.1, all variables in the context should be of type dyn, and all results should
be of type dyn.
Task 3.6 (30 pts). Implement the translation in translate/translate.fun .
Note that you should use the syntax extensions in translate/synext.sml . You will not need to
define your own labels for any purposes.
Testing Load translate/sources.cm . Then, you can test using InterpreterTranslate ,
which translates REPL and file inputs from PyCF to FPC before evaluation.
– InterpreterTranslate.repl ();
-> False if False else True;
(If ((Bool false), (Bool false), (Bool true)))
Type (source): ok
Compiling …
(* result of translating into FPC *)
Type (target): (Rec (d3064 . (Sum [“bool” ↪→ (Sum [“false” ↪→ (Prod
[]), “true” ↪→ (Prod [])]), “fun” ↪→ (Arrow (d3064 , d3064)),
“int” ↪→ Int , “list” ↪→ (List d3064)])))
Evaluating … val (Fold ((Inj (“bool”, (Inj (“true”, (Pair
Notice that the type of the translated code and the result of evaluating the translated code are
dyn; this should always be the case. Additionally, notice that the value is simply:
fold[ d . dynview[d] ]( bool · true )
Type annotations are not printed, since they are very long and obfuscate the output.
3.5 Reflection
Observe that the compiled code for seemingly-simple PyCF code becomes massive, due to the class
tagging and checking. Consider the following function:
# Sum the numbers from 0 to n.
def triangle(n):
return 0 if n <= 0 else n + triangle(n + -1) One invariant of triangle is that it always returns an object of class int. However, in PyCF, we must perform many redundant tag checks at run-time; for example, we must check at each layer of recursion that both n and triangle(n + -1) are of class int before adding them together. In PyCF, there’s no way for us to get around these checks. However, if we work in FPC, we can wrap efficient code so it is compatible with compiled PyCF code. Continuing our example, consider an efficient (class-check free) version of the given function, etri: etri ≜ fun[ int ; int ]( f . n . if( leq(n ; int[ 0 ] ) ; int[ 0 ] ; plus(n ; ap( f ; plus(n ; int[−1 ] ) ) ) ) ) This code isn’t immediately compatible with compiled PyCF code, since it does not have type dyn. However, we can wrap etri such that it becomes compatible while still maintaining efficiency in the “inner loop” of computation.4 Task 3.7 (5 pts). Define efficient code edyn-tri : dyn (i.e., compatible with “dynamically typed” code) to compute a triangle number using the efficient triangle number function etri : int → int. Dynamically invoking edyn-tri should perform a constant number of tags and casts, instead of per- forming tags and casts at each layer of recursion like the naive compiled code. Hint. Your solution shouldn’t depend on the implementation of etri; in fact, it should work for any expression of type int → int. 4This is how some Python libraries, such as NumPy, manage to run fast: they use efficient C code under the hood which is wrapped in PyObject compatibility code. https://github.com/numpy/numpy A Definition of PyCF A.1 Grammar The grammar is given in Section 2.1. A.2 Dynamics A.2.1 Tag Refutation bool[ b ] isnt int bool[ b ] isnt list bool[ b ] isnt fun int[ i ] isnt bool int[ i ] isnt list int[ i ] isnt fun d0 val . . . dn−1 val list( d0 ; . . . ; dn−1 ) isnt bool d0 val . . . dn−1 val list( d0 ; . . . ; dn−1 ) isnt int d0 val . . . dn−1 val list( d0 ; . . . ; dn−1 ) isnt fun fun( f . x . d ) isnt bool fun( f . x . d ) isnt int fun( f . x . d ) isnt list A.2.2 Stepping d val d err d 7−→ d′ bool[ b ] val if( d ; d1 ; d0 ) 7−−→ if( d′ ; d1 ; d0 ) if( d ; d1 ; d0 ) err if( bool[ true ] ; d1 ; d0 ) 7−−→ d1 if( bool[ false ] ; d1 ; d0 ) 7−−→ d0 int[ i ] val d1 7−−→ d′1 plus( d1 ; d2 ) 7−−→ plus( d′1 ; d2 ) plus( d1 ; d2 ) err d1 val d2 7−−→ d′2 plus( d1 ; d2 ) 7−−→ plus( d1 ; d′2 ) d1 val d2 err plus( d1 ; d2 ) err plus( int[ i1 ] ; int[ i2 ] ) 7−−→ int[ i1 + i2 ] dj val (for all 0 ≤ j < m) d′j val (for all 0 ≤ j < n) plus( list( d0 ; . . . ; dm−1 ) ; list( d 0 ; . . . ; d n−1 ) ) 7−−→ list( d0 ; . . . ; dm−1 ; d′0 ; . . . ; d′n−1 ) d val d isnt int plus( int[ i ] ; d ) err dj val (for all 0 ≤ j < m) d val d isnt list plus( list( d0 ; . . . ; dm−1 ) ; d ) err d1 val d2 val d1 isnt int d1 isnt list plus( d1 ; d2 ) err d1 7−−→ d′1 leq( d1 ; d2 ) 7−−→ leq( d′1 ; d2 ) leq( d1 ; d2 ) err d1 val d2 7−−→ d′2 leq( d1 ; d2 ) 7−−→ leq( d1 ; d′2 ) d1 val d2 err leq( d1 ; d2 ) err leq( int[ i1 ] ; int[ i2 ] ) 7−−→ bool[ true ] leq( int[ i1 ] ; int[ i2 ] ) 7−−→ bool[ false ] d1 isnt int leq( d1 ; d2 ) err d2 isnt int leq( int[ i1 ] ; d2 ) err dj val (for all 0 ≤ j < k) dk 7−−→ d′k d m = dm (for all m ̸= k) list( d0 ; . . . ; dn−1 ) 7−−→ list( d′0 ; . . . ; d′n−1 ) dj val (for all 0 ≤ j < k) dk err list( d0 ; . . . ; dn−1 ) err dj val (for all 0 ≤ j < n) list( d0 ; . . . ; dn−1 ) val index( d ; dindex ) 7−−→ index( d′ ; dindex ) index( d ; dindex ) err d val dindex 7−−→ d′index index( d ; dindex ) 7−−→ index( d ; d′index ) d val dindex err index( d ; dindex ) err dj val (for all 0 ≤ j < n) 0 ≤ i < n index( list( d0 ; . . . ; dn−1 ) ; int[ i ] ) 7−−→ di dj val (for all 0 ≤ j < n) ¬(0 ≤ i < n) index( list( d0 ; . . . ; dn−1 ) ; int[ i ] ) err d val d isnt list dindex val index( d ; dindex ) err dj val (for all 0 ≤ j < n) dindex val dindex isnt int index( list( d0 ; . . . ; dn−1 ) ; dindex ) err len( d ) 7−−→ len( d′ ) len( d ) err dj val (for all 0 ≤ j < n) len( list( d0 ; . . . ; dn−1 ) ) 7−−→ int[n ] d val d isnt list len( d ) err fun( f . x . d ) val ap( d ; d1 ) 7−−→ ap( d′ ; d1 ) ap( d ; d1 ) err d val d1 7−−→ d′1 ap( d ; d1 ) 7−−→ ap( d ; d′1 ) d val d1 err ap( d ; d1 ) err ap( fun( f . x . d2 ) ; d1 ) 7−−→ {fun( f . x . d2 ), d1/f, x}d2 d val d isnt fun d1 val ap( d ; d1 ) err d1 7−−→ d′1 let( d1 ; x . d2 ) 7−−→ let( d′1 ; x . d2 ) let( d1 ; x . d2 ) 7−−→ {d1/x}d2 let( d1 ; x . d2 ) err isinstance[ c ]( d ) 7−−→ isinstance[ c ]( d′ ) isinstance[ c ]( d ) err isinstance[ bool ]( bool[ b ] ) 7−−→ bool[ true ] d isnt bool isinstance[ bool ]( d ) 7−−→ bool[ false ] isinstance[ int ]( int[ i ] ) 7−−→ bool[ true ] d isnt int isinstance[ int ]( d ) 7−−→ bool[ false ] dj val (for all 0 ≤ j < n) isinstance[ list ]( list( d0 ; . . . ; dn−1 ) ) 7−−→ bool[ true ] d isnt list isinstance[ list ]( d ) 7−−→ bool[ false ] isinstance[ fun ]( fun( f . x . d ) ) 7−−→ bool[ true ] d isnt fun isinstance[ fun ]( d ) 7−−→ bool[ false ] B Definition of FPC In our formulation of FPC, we have: • labeled products and sums, where there is a sort of labels which we assume are ordered • a run-time error construct which causes the program to halt • integer and list primitives B.1 Grammar Sort Abstract form Concrete form Label l ::= . . . . . . (labels) Typ τ ::= int int (primitive) list( τ ) τ list (primitive) prod( l ↪→ τl | l ∈ L ) ⟨τl⟩l∈L sum( l ↪→ τl | l ∈ L ) [τl]l∈L arr( τ1 ; τ2 ) τ1 → τ2 rec( t . τ ) rec t is τ Exp e ::= x x error[ τ ] error[ τ ] int[ i ] i (. . . ,−2,−1, 0, 1, 2, . . . ) plus( e1 ; e2 ) e1 + e2 (integer addition) leq( d1 ; d2 ) d1 <= d2 list( e0 ; . . . ; en−1 ) [e0 ; . . . ; en−1] append( e1 ; e2 ) e1 @ e2 index( e ; eindex ) e[eindex] len( e ) len(e) tpl( l ↪→ el | l ∈ L ) ⟨l ↪→ el | l ∈ L⟩ (labeled tuple) pr[ l ]( e ) e · l (projection from a labeled prod.) in[ l ][ (l ↪→ τl)l∈L ]( e ) l · e (injection into a labeled sum) case( e ; l ↪→ xl . el | l ∈ L ) case e {l · xl ↪→ el | l ∈ L} (labeled case) fold[ t . τ ]( e ) fold( e ) unfold( e ) unfold( e ) λ[ τ ](x . e ) λ (x : τ ) e ap( e ; e1 ) e( e1 ) B.2 Statics B.2.1 Type Well-formedness ∆ ⊢ τ type Informally: “τ only uses type variables present in ∆”, where ∆ ::= t1 type, . . . , tn type. ∆, t type ⊢ t type ∆ ⊢ int type ∆ ⊢ τ type ∆ ⊢ list( τ ) type ∆ ⊢ τl type (for all l ∈ L) ∆ ⊢ prod( l ↪→ τl | l ∈ L ) type ∆ ⊢ τl type (for all l ∈ L) ∆ ⊢ sum( l ↪→ τl | l ∈ L ) type ∆ ⊢ τ1 type ∆ ⊢ τ2 type ∆ ⊢ arr( τ1 ; τ2 ) type ∆, t type ⊢ τ type ∆ ⊢ rec( t . τ ) type B.2.2 Expression Typing Γ, x : τ ⊢ x : τ Γ ⊢ error[ τ ] : τ Γ ⊢ int[ i ] : int Γ ⊢ e1 : int Γ ⊢ e2 : int Γ ⊢ plus( e1 ; e2 ) : int Γ ⊢ e1 : int Γ ⊢ e2 : int Γ ⊢ leq( e1 ; e2 ) : bool Note, we are use the following abbreviation: unit ≜ prod( l ↪→− | l ∈ ∅ ) (empty labeled product) bool ≜ sum( l ↪→ unit | l ∈ true, false ) ⊢ τ type Γ ⊢ ej : τ (for all 0 ≤ j < n) Γ ⊢ list( e0 ; . . . ; en−1 ) : list( τ ) Γ ⊢ e1 : list( τ ) Γ ⊢ e2 : list( τ ) Γ ⊢ append( e1 ; e2 ) : list( τ ) Γ ⊢ e : list( τ ) Γ ⊢ eindex : int Γ ⊢ index( e ; eindex ) : τ Γ ⊢ e : list( τ ) Γ ⊢ len( e ) : int ⊢ τ1 type Γ, x : τ1 ⊢ e : τ2 Γ ⊢ λ[ τ1 ](x . e ) : arr( τ1 ; τ2 ) Γ ⊢ e : arr( τ1 ; τ2 ) Γ ⊢ e1 : τ1 Γ ⊢ ap( e ; e1 ) : τ2 Γ ⊢ el : τl (for all l ∈ L) Γ ⊢ tpl( l ↪→ el | l ∈ L ) : prod( l ↪→ τl | l ∈ L ) Γ ⊢ e : prod( l ↪→ τl | l ∈ L ) Γ ⊢ pr[ l ]( e ) : τl ⊢ τl type (for all l ∈ L) Γ ⊢ e : τl Γ ⊢ in[ l ][ (l ↪→ τl)l∈L ]( e ) : sum( l ↪→ τl | l ∈ L ) ⊢ τ type Γ ⊢ e : sum( l ↪→ τl | l ∈ L ) Γ, xl : τl ⊢ el : τ (for all l ∈ L) Γ ⊢ case( e ; l ↪→ xl . el | l ∈ L ) : τ t type ⊢ τ type Γ ⊢ e : {rec( t . τ )/t}τ Γ ⊢ fold[ t . τ ]( e ) : rec( t . τ ) Γ ⊢ e : rec( t . τ ) Γ ⊢ unfold( e ) : {rec( t . τ )/t}τ B.3 Dynamics error[ τ ] err int[ i ] val e1 7−−→ e′1 plus( e1 ; e2 ) 7−−→ plus( e′1 ; e2 ) e1 val e2 7−−→ e′2 plus( e1 ; e2 ) 7−−→ plus( e1 ; e′2 ) plus( int[ i1 ] ; int[ i2 ] ) 7−−→ int[ i1 + i2 ] e1 7−−→ e′1 leq( e1 ; e2 ) 7−−→ leq( e′1 ; e2 ) e1 val e2 7−−→ e′2 leq( e1 ; e2 ) 7−−→ leq( e1 ; e′2 ) leq( int[ i1 ] ; int[ i2 ] ) 7−−→ true leq( int[ i1 ] ; int[ i2 ] ) 7−−→ false Note, we are use the following abbreviation: triv ≜ tpl( l ↪→− | l ∈ ∅ ) (empty labeled tuple) true ≜ in[ true ][ true, false ]( triv ) false ≜ in[ false ][ true, false ]( triv ) ej val (for all 0 ≤ j < k) ek 7−−→ e′k e m = em (for all m ̸= k) list( e0 ; . . . ; en−1 ) 7−−→ list( e′0 ; . . . ; e′n−1 ) ej val (for all 0 ≤ j < k) ek err list( e0 ; . . . ; en−1 ) err ej val (for all 0 ≤ j < n) list( e0 ; . . . ; en−1 ) val e1 7−−→ e′1 append( e1 ; e2 ) 7−−→ append( e′1 ; e2 ) e1 val e2 7−−→ e′2 append( e1 ; e2 ) 7−−→ append( e1 ; e′2 ) ej val (for all 0 ≤ j < m) e′j val (for all 0 ≤ j < n) append( list( e0 ; . . . ; em−1 ) ; list( e 0 ; . . . ; e n−1 ) ) 7−−→ list( e0 ; . . . ; em−1 ; e 0 ; . . . ; e index( e ; eindex ) 7−−→ index( e′ ; eindex ) e val eindex 7−−→ e′index index( e ; eindex ) 7−−→ index( e ; e′index ) ej val (for all 0 ≤ j < n) 0 ≤ i < n index( list( e0 ; . . . ; en−1 ) ; int[ i ] ) 7−−→ ei ej val (for all 0 ≤ j < n) ¬(0 ≤ i < n) index( list( e0 ; . . . ; en−1 ) ; int[ i ] ) err len( e ) 7−−→ len( e′ ) len( e ) err ej val (for all