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 where
T ≜ rectisτ,
τ ≜E,→unit+N,→t×bool×t.
The meaning of this type depends on whether FPC is understood eagerly/by-value or lazily/by- name.
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):ρ
1 lg n is the base-2 logarithm of n. For simplicity, your implementation may do anything when n ≤ 0. 2
and the following dynamics:
Trec[ ρ ]( Emp ; x . e2 ) 7−→ let x be E · ⟨⟩ in e2
r1 =Trec[ρ](t1 ;x.e2) r2 =Trec[ρ](t2 ;x.e2)
Trec[ ρ ]( Node(t1, b, t2) ; x . e2 ) 7−→ let x 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 values.
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
Your solution will follow very closely the dynamics, using let to bind the results of the
Trec[ρ](e1 ;x.e2)≜unroll(R)(e1). 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:
unfold(Tgen[σ](e1 ;x.e2))7−→case{e1/x}e2{E· ,→E·⟨⟩|N·⟨s1,b,s2⟩,→N·⟨t1,b,t2⟩}
t1 =Tgen[σ](s1 ;x.e2) t2 =Tgen[σ](s2 ;x.e2)
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 int int
list list fun fun
Object d ::= x x bool[ b ] b
if(d;d1;d0) d1ifdelsed0 int[i] i
plus( d1 ; d2 ) d1+d2
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 )
ap( d ; d1 ) d( d1 )
let(d1 ;x.d2 )
isinstance[ c ]( d ) isinstance(d, c)
(True, False) (...,−2,−1,0,1,2,...)
(int addition and list append)
(see below) (see below)
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] : 5
程序代写 CS代考 加QQ: 749389476
# 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):
disntc disnotofclassc
d err Task 2.1 (20 pts). Implement the
d is a closed value d steps to d′
d incurs a run-time error
, Fun , Ap , and IsInstance cases of the dynamics of
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.
lang-pycf/dynamics-pycf.sml
- InterpreterPyCF.repl ();
-> 1 + 2 + 3;
(Plus ((Plus ((Int 1), (Int 2))), (Int 3))) Type: ok
Evaluating… val (Int 6)
-> [1, 2] + [3];
(Plus ((List [(Int 1), (Int 2)]), (List [(Int 3)]))) Type: ok
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)))))) Type: ok
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). 7
浙大学霸代写 加微信 cstutorcs
• 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)])])))))) Type: ok
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:
where we define:
τbool ≜ bool τint ≜ int
τlist ≜ list( dyn )
τfun ≜ arr( dyn ; dyn ))
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- tion.
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 Γ ⊢ e : dyn
Γ ⊢ new[c](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 dyn.
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 rule:
Γ,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:
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.
# Sum the numbers from 0 to n.
def triangle(n):
return 0 if n <= 0 else n + triangle(n + -1)
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
int[i] isnt bool
bool[ b ] isnt list
int[i] isnt list
d0 val ... dn−1 val list(d0 ;...;dn−1)isntint
fun( f . x . d ) isnt int
bool[ b ] isnt fun
int[i] isnt fun
d0 val ... dn−1 val list(d0 ;...;dn−1)isntfun
fun( f . x . d ) isnt list
d err if(d;d1 ;d0)err
d0 val ... dn−1 val list(d0 ;...;dn−1)isntbool
fun( f . x . d ) isnt bool A.2.2 Stepping
d err d 7−→ d′
bool[b]val if(d;d1 ;d0)7−→if(d′ ;d1 ;d0)
if(bool[true];d1 ;d0)7−→d1
if(bool[false];d1 ;d0)7−→d0
d 1 7 − −→ d ′1
int[i]val plus(d1 ;d2)7−→plus(d′1 ;d2) plus(d1 ;d2)err
d1 val d2 err
d1 val d2 7−→ d′2
plus(d1 ;d2)7−→plus(d1 ;d′2) plus(d1 ;d2)err plus(int[i1];int[i2])7−→int[i1 +i2]
dj val(forall0≤j