Coursework
CM50262 Functional Programming
Coursework
Due: 8pm, 30 April 2021
Complete part A in the file Coursework.hs , and part B in a separate PDF. Submit both on Moodle by Friday 30 April 8pm. Make sure your file does not have syntax errors or type errors; where necessary, comment out partial solutions. Use the provided function names. You may use auxiliary functions, and you are encouraged to add your own examples and tests.
Assessment and feedback Your work will be judged primarily on the correctness of your solutions. Incorrect or partial solutions may be given partial marks if they operate correctly on certain inputs. Marking is part-automated, part-manual. You will receive individual marks, and we will publish an overall feedback document.
Plagiarism warning The assessed part of this coursework is an individual assignment. Collaboration is not permitted: you should not discuss your work with others, and the work you submit should be your own. Disclosing your solutions to others, and using other people’s solutions in your work, both constitute plagiarism: see http://www.bath.ac.uk/quality/documents/QA53.pdf.
Type inference (80 marks)
Type inference is the process of finding a type for a λ-term. In this coursework we will implement a simple and transparent version of it. In the file Coursework.hs , you are started off with the implementation of the λ-calculus from the tutorials. The work is split up into several assignments. These do not always build on each other, or sometimes only partly, so if you get stuck, please do attempt the next assignment.
Types with variables
Types are defined by the following grammar, where A = {α, β, γ, . . . } is a set of type variables, here called atoms.
ρ,σ,τ,υ ::= α ∈A | σ→τ
You are given a data type Type that implements the above definition, with a Show instance for pretty printing. The set of atoms is given by the type Atom , a synonym for String . The list atoms can be used to generate a fresh atom when needed. There are two example types:
*Main> t1
a -> b
*Main> t2
(c -> d) -> e
Instructions
Coursework CM50262 Functional Programming
Note that the type constructor :-> is infix. The patterns for Type are as follows. At x
x :-> y
The declaration infixr 5 :-> moreover tells the compiler that :-> is right-associative,
like the arrow type of the λ -calculus, which means that: r :-> s :-> t == r :-> (s :-> t)
Assignment 1 (10 marks):
a) Complete the function occurs that determines if an atom occurs in a type.
b) Complete the function findAtoms that returns the atoms occurring in a type in an
(alphabetically) ordered list.
*Main> occurs “a” t1
True
*Main> occurs “b” t2
False
*Main> findAtoms t1
[“a”,”b”]
*Main> At “a” :-> t2 :-> t1
a -> ((c -> d) -> e) -> a -> b
*Main> findAtoms it
[“a”,”b”,”c”,”d”,”e”]
Substitutions
Substitution for types is simpler than for terms, since there is no variable capture, and so no need for capture-avoidance. The definition is:
α[τ/α]= τ
β[τ/α]= β
(ρ → σ)[τ/α]= ρ[τ/α] → σ[τ/α]
A series of substitutions is abbreviated by S :
S = [τ1/α1] . . . [τn/αn]
(if α ̸= β)
Coursework CM50262 Functional Programming
The empty series of substitutions, which represents the substitution that does nothing, is written as ε. Then τ[S] is τ with the substitutions in S applied to it, so that τ[ε] = τ , and if S is as above,
τ[S] = τ[τ1/α1]…[τn/α1] .
We will give a substitution [τ/α] as a pair (a,t) of an Atom a and a Type t. A
series of substitutions will be a list of such pairs (note that the order is reversed):
S = [τ1/α1] . . . [τn/αn] [ (an,tn) , … , (a1,t1) ] Assignment 2 (10 marks):
You are given a type Sub for substitutions, as a pair of an Atom and a Type , and three examplesubstitutions s1, s2,and s3.
a) Complete the function sub that applies a substitution to a type.
b) Complete the function subs that applies a list of substitutions to a type, with the head
of the list applied last, and the tail applied first.
*Main> sub s1 t1
e -> b
*Main> sub s2 t2
(c -> d) -> b -> c
*Main> sub s3 t3
a -> (a -> a) -> a -> a
*Main> subs [s1] t1
e -> b
*Main> subs [s2,s1] t1
(b -> c) -> b
*Main> subs [s3,s2,s1] t1
(b -> a -> a) -> b
*Main> subs [s1,s2,s3] t3
e -> (e -> e) -> e -> e
*Main> subs [s3,s2,s1] t3
(b -> a -> a) -> (a -> a) -> a -> a
Coursework CM50262 Functional Programming
Unification
To find a type for a term, we have to solve the following problem. First, an example. Suppose we have the function N = λx.λy.xyy with type (α→α→β)→α→β, and we want to supply it with the argument M = λz.λw.z with the type γ → δ → γ. To make this possible, informally we can observe that N and M can also be given the types:
N : (α→α→α)→α→α M : α→α→α
These match: N can be applied to M, with the type NM : α→α. To obtain these matching types from the original ones in a more formal way, we use the series of substitutions S = [α/β][α/γ][α/δ] , which replaces each occurrence of β , γ , and δ with α . When used on both original types, we get the desired types for N and M :
((α→α→β)→α→β)[S] = (α→α→α)→α→α (γ→δ→γ)[S] = α→α→α
This is the general problem: if we have N : σ → τ and M : ρ , to give a type to N M we need to find substitutions S such that σ[S] = ρ[S], and then we will have N M : τ[S]. (The reason that we can use substitution to make types equal, is that if a term N has type τ , then it can also be given the more special type τ[S] for any substitutions S .)
The algorithm that finds S is called unification, and the substitutions S that give ρ[S] = σ[S] are called a unifier of ρ and σ . Here are a few observations for how it should work.
• A unifier for a variable α and any type τ can be just the substitution [τ/α], since α[τ/α] = τ .
• Unless τ contains the variable α , for example if τ = β → α . In that case, (β → α)[β → α/α] = β → β → α while α[β → α/α] = β → α , and these
are not equal. Then, unification fails: α and β → α cannot be unified.
• Unless τ is just α itself, since α can be unified with itself by the empty substitution
series ε.
• A unifier for two types that are not variables, σ1 →σ2 and τ1 →τ2, must be a
substitution series S such that σ1[S] = τ1[S] and σ2[S] = τ2[S] .
This last case shows that the algorithm needs to find a unifier not just for a single pair of types, but for a set of pairs of types. The four cases above then show what steps it must take: if a pair is of the form
• α and α , discard it; otherwise
Coursework CM50262 Functional Programming
• α and τ containing α , fail to unify these terms;
• α and τ not containing α , return the unifier [τ /α] ;
• σ1 →σ2 and τ1 →τ2,continuetounifyboththepair σ1 and τ1 andthepair σ2 and τ2 .
We will now formalize the unification algorithm. We will write a pair of types σ and τ that we want to unify as σ ↔ τ , and call it a unification pair. The algorithm is then defined using states and transitions. A state is a pair (S,U) where
• S is a series of subsitutions, which is the solution so far;
• U = {σ1 ↔ τ1,…,σn ↔ τn} is a set of unification pairs.
To unify σ and τ the algorithm starts from (ε, {σ ↔ τ }) . The transitions are as follows: oninput (S,{u}∪U),iftheunificationpair u isoftheform
a) α↔α:return(S,U);
b) α↔τorτ↔α:ifαoccursinτ,FAIL;
otherwise, return (S[τ/α],U[τ/α])
c) (σ1→σ2)↔(τ1→τ2):return(S,{σ1↔τ1,σ2↔τ2}∪U)
Here, S[τ/α] is the series of substitution S with [τ/α] added at the end, and U[τ/α] is the set of unification pairs U with [τ/α] applied to every type in every pair. The unification process is complete when a state (S, ∅) is reached, with an empty set of unification pairs. The algorithm then returns S as the unifier.
Assignment 3 (20 marks):
To implement and test the unification algorithm, you are given a type Upair for unification pairs, a type State for the internal state of the algorithm, example unification pairs u1 through u4 , and example state st1 .
a) Complete the function sub_u that applies a substitution [τ/α] to a list of unification pairs U as U[τ/α].
b) Complete the function step that carries out a single transition of the unification algo- rithm as described above. For the case of a FAIL, you may throw an error.
c) Complete the function unify that does the following:
• Given a list of unification pairs U , start the algorithm with the state (ε,U)
Coursework
CM50262 Functional Programming
• If the current state is (S, ∅) , return S .
• Otherwise, apply a transition and try again.
*Main> sub_u s1 [u1,u2]
[(e -> b,c),(e -> e,e -> c)]
*Main> sub_u s3 [u4]
[(((a -> a) -> d) -> e,a -> (a -> a) -> a -> a)]
*Main> st1 — highlighting the next unification pair
([],[(a -> b,c),(a -> a,a -> c)])
*Main> step it
([(“c”,a -> b)],[(a -> a,a -> a -> b)])
*Main> step it
([(“c”,a -> b)],[(a,a),(a,a -> b)])
*Main> step it
([(“c”,a -> b)],[(a,a -> b)])
*Main> step it
*** Exception: Step: atom a occurs in a -> b
*Main> unify [u3,u4]
[(“e”,c -> c),(“b”,e),(“a”,c -> d)]
*Main> let s = it
*Main> subs s t1
(c -> d) -> c -> c
*Main> subs s t2
(c -> d) -> c -> c
*Main> subs s t3
(c -> d) -> c -> c
Derivations
To give a term a type is done by a typing derivation. We need the following notions:
• A context Γ = x1 : τ1,…,xn : τn is a sequence of variables x1 through xn each with an assigned type τ1 through τn . The order of variables is not important, and it is assumed that variables don’t occur more than once.
• Ajudgement Γ⊢N :τ assignsaterm N thetype τ inthecontext Γ.
• A derivation is a proof that a judgement holds, and is built from the following typing
— case b)
— case c)
— case a)
— case b), FAIL
Coursework CM50262 Functional Programming
rules, called axiom, abstraction, and application
Γ, x : σ ⊢ M : τ Γ,x : τ ⊢ x : τ Γ ⊢ λx.M : σ → τ
Γ ⊢ M : σ → τ Γ ⊢ N : σ Γ ⊢ MN : τ
axiom abstraction
An example derivation for the term (λx. x) y is as follows.
application
y : α, x : α ⊢ x : α
y : α ⊢ λx. x : α → α y : α ⊢ y : α
y : α ⊢ (λx. x) y : α
Assignment 4 (15 marks):
a) Complete the following types:
• The type synonym Context for contexts as lists of pairs of a variable and a type. (In your file, Context is set to the unit type () as a default; you should replace this with your own type.)
• The type synonym Judgement for judgements as a triple of a context, a term, and a type.
• The data type Derivation for derivations, with the three constructors Axiom , Abstraction , and Application for each of the typing rules. Each construc- tor should take as arguments: a Judgement for the conclusion of the rule, and for each premise of the typing rule a Derivation .
Un-comment the test derivations d1 and d2 to check your definition. If the file does not typecheck, inspect d1 and d2 to find the correct type definitions.
Un-comment also the Show instance for Derivation , under the header “Typesetting derivations” in your Coursework.hs file, for pretty derivations. Evaluate d1 and d2
to see what it does.
b) Complete the function conclusion that extracts the concluding Judgement from a derivation.
c) Complete the three functions subs_ctx , subs_jdg , and subs_der that apply a list of substitutions to every Type in respectively a Context , a Judgement , and a Derivation . Like your earlier function subs (which you may use here) the substitution at the head of the list should be applied last.
Coursework
CM50262 Functional Programming
*Main> d1
——————–
x: a , y: a |- x : a ———————- ————- y:a|-\x.x:a->a y:a|-y:a ————————————-
y: a |- (\x. x) y : a
*Main> conclusion d2
([(“y”,b)],(\x. x y) (\z. z),a)
*Main> subs_jdg [s2,s1] it
([(“y”,b)],(\x. x y) (\z. z),b -> c)
*Main> subs_jdg [(“b”,At “d” :-> At “e”)] it
([(“y”,d -> e)],(\x. x y) (\z. z),(d -> e) -> c)
*Main> subs_der [s2,s1] d1
———————————–
x: b -> c , y: b -> c |- x : b -> c ————————————— ———————– y:b->c|-\x.x:(b->c)->b->c y:b->c|-y:b->c —————————————————————-
y: b -> c |- (\x. x) y : b -> c
Type inference
In this final part we will construct a type derivation for a λ-term, if it can be typed. The process will be as follows:
• First, build an incomplete derivation where every type is an atom, following the incom- plete typing rules below. An example of such an incomplete derivation is d2 .
• From this derivation, extract a set of unification pairs U , one for each rule, according to the table below.
• From this set U construct a unifier S , if one exists, using the algorithm from the section Unification.
Coursework CM50262 Functional Programming
• Apply the substitutions in S to the incomplete derivation, using the algorithms from the previous section, Derivations.
Incomplete rules
Γ,x:α⊢x:β Γ, x : α ⊢ M : β
Γ⊢λx.M :γ Γ⊢M:γ Γ⊢N:α
Unification pairs
α ↔ β γ↔α→β
γ↔α→β
The result of this process, if it is successful, is a derivation; moreover, it is guaranteed to find
Γ ⊢ MN : β a derivation if one exists.
Assignment 5 (25 marks):
a) Complete the function derive0 that creates an incomplete derivation from a λ -term where all types are ‘empty’, as At “” . To manage contexts, use the auxiliary func- tion aux to build a derivation from a Judgement instead of a term. Make sure the contexts hold the correct variables. In the abstraction case, for a term λx.N , if x already occurs in the context, replace the old occurrence instead of adding a second x (the new x does not have to be in the same place as the old one). Initially, the context should hold the free variables of the input term.
b) Complete the function derive1 that creates an incomplete derivation from a λ -term where all types are atoms, following the rules above. Use your derive0 as an ex- ample to expand on (not as an auxiliary function to call). Make sure that all atoms you introduce are fresh, using the list atoms as a supply. Initially, assign an atom from atoms to the term itself and to each free variable in the context, and provide the re- maining atoms to aux . To provide distinct atoms to the two premises of an application, you can split a stream of atoms in two by selecting the even-positioned atoms for one stream, and the odd-positioned ones for the other:
α,β,γ,δ,ε, … →
α,γ,ε, … β,δ, …
c) Complete the function upairs that extracts the type unification pairs from an incom- plete derivation. You may assume that the derivation is generated by derive1 , and follows the incomplete rules above. (That is, you don’t have to check the entire context from one rule to another, only the type of the term and of the abstracted variable in an abstraction rule.)
Coursework CM50262 Functional Programming
d) Complete the function derive that takes a term and produces a type derivation for it, if one exists. (If none exists, you may throw an error.) Do this by generating an incomplete derivation with derive1 , extracting the unification pairs with upairs , unifying them with unify , and applying the resulting substitutions to the incomplete derivation with subs_der .
Note that in your solutions, you do not have to have the same type variables, as long as they are the same up to renaming.
*Main> derive0 n1
—————–
x: ,y: |-x: —————– ———–
y: |-\x.x: y: |-y: —————————–
y: |-(\x.x)y:
*Main> derive1 n1 — You may have different atoms,
— but they must all be distinct
——————–
x: f , y: b |- x : h
——————– ————-
y: b |- \x. x : c y: b |- y : d
———————————-
y: b |- (\x. x) y : a
*Main> upairs it — You may have a different order
[(c,d -> a),(c,f -> h),(h,f),(d,b)]
*Main> upairs d2 — You may have a different order
[(c,h -> a),(c,d -> e),(f,g -> e),(f,d),(g,b),(h,i -> j),(j,i)]
*Main> derive n1 — You may have different atoms
——————–
x: b , y: b |- x : b ———————- ————- y:b|-\x.x:b->b y:b|-y:b ————————————-
y: b |- (\x. x) y : b