计算机代写do not hesitate to contact me!
WeChat：lovexc60
COMP3161/9164 20T3 Assignment 2
Type Inference for Polymorphic MinHs

1 Task 1
Task 1 is worth 100% of the marks of this assignment. You are to implement type inference for
MinHS with aggregate data structures. The following cases must be handled:
• the MinHS language of the first task of assignment 1 (without n-ary functions or letrecs, or
lists)
• product types: the 0-tuple and 2-tuples.
• sum types
1
• polymorphic functions
These cases are explained in detail below. The abstract syntax defining these syntactic entities is
in Syntax.hs. You should not need to modify the abstract syntax definition in any way.
Your implementation is to follow the definition of algebraic data types found in the lecture on
data structures, and the rules defined in the lectures on type inference. Additional material can be
found in the lecture notes on polymorphism, and the reference materials. The full set of rules is
outlined in this specification.
2 Bonus Tasks
These tasks are all optional, and are worth a total of an additional 10%.
2.1 Bonus Task 1: Simple Syntax Extensions
This bonus task is worth an additional 3%. In this task, you should implement type inference for
n-ary functions, and multiple bindings in the one let expression, with the same semantics as the
extension tasks for Assignment 1.
You will need to develop the requisite extensions to the type inference algorithm yourself, but
the extensions are very similar to the existing rules.
2.2 Bonus Task 2: Recursive Bindings
This bonus task is worth an additional 3%. In this task you must implement type inference for
letrec constructs.
Each binding will require a fresh unification variable, similar to multiple-binding let expressions,
however for letrec we do not wish types to be generalised.
2.3 Bonus Task 3: User-provided type signatures
This bonus task is worth an additional 4%. In this task you are to extend the type inference pass
to accept programs containing some type information. You need to combine this with the results
of your type inference pass to produce the final type for each declaration. That is, you need to be
able to infer correct types for programs like:
main = let f :: (Int -> Int)
= recfun g x = x;
in f 2;
You must ensure that the type signatures provided are not overly general. For example, the following
program should be a type error, as the user-provided signature is too general:
main :: (forall a. a) = 3;
3 Algebraic Data Types
This section covers the extensions to the language of the first assignment. In all other respects
(except lists) the language remains the same, so you can consult the reference material from the
first assignment for further details on the language.
2
3.1 Product Types
We only have 2-tuples in MinHS, and the Unit type, which could be viewed as a 0 type.
Types τ → τ 1 * τ 2
| 1
Expressions exp → (e1, e2)
| fst e | snd e
| ()
3.2 Sum Types
Types τ → τ + τ
Expressions exp → Inl e1
| Inr e2
| case e of
Inl x -> e1 ;
Inr y -> e2 ;
3.3 Polymorphism
The extensions to allow polymorphism are relatively minor. Two new type forms have been introduced: the TypeVar t form, and the Forall t e form.
Types τ → forall τ. ..τ..
For example, consider the following code fragment before and after type inference:
main =
let f = recfun g x = x;
in if f True
then f (Inl 1)
else f (Inr ());
main :: (Int + 1) =
let f :: forall a. (a -> a) = recfun g :: (a -> a) x = x;
in if f True
then f (Inl 1)
else f (Inr ());
3