## Description

In this assignment, you will construct a constraint solver and a few unification algorithms.

You will implement four modules: Unify, Equation, Tree, and Natural. You should submit

each in its own *.hs or *.lhs file. File names are case sensitive.

Note: All function definitions at top level must have explicit type annotations. Unless

otherwise specified, your solutions may utilize functions from the standard prelude as well as

material from the lecture notes and textbook. You may not use any other materials without

explicit citation.

## Problem 1. (5 pts)

A substitution is any mapping (in a mathematical sense) of variables to values. Substitutions

can be represented in various ways. We will represent a substitution by a list of pairs.

In each pair in the list, the first component specifies a variable name as a string and the

second component specifies the value to which that variable is mapped. For example, the

substitution

[(“x”, 1), (“y”, 2)]

indicates that all instances of “x” map to 1 and all instances of “y” map to 2. To apply

a substitution is to replace all variables in a data type instance (i.e. a value) with their

corresponding value in the substitution. You should introduce into your Unify module the

following type synonym declaration:

type Subst a = [(String, a)]

Unification is defined in terms of substitutions. We say a substitution s unifies two values

v1 and v2 if

subst s v1 == subst s v2,

where (==) is derived equality on the type of those values and subst s v is the application

of a substitution s on a value v. You will define a representation for substitutions in the

Unify module.

(a) Define a value emp::Subst a that represents the empty substitution, and a function

sub::String -> a -> Subst a for constructing a substitution for only a single variable.

(b) Define a function get::String -> Subst a -> Maybe a that takes a variable name

and a substitution, and returns the value for which that variable must be substituted.

If the substitution is not defined on the variable, the function should return Nothing.

## Problem 2. (15 pts)

Because every data type has different constructors, each data type requires its own specific

definition of a substitution function. However, we may want to write polymorphic code that

uses substitutions and performs unification without explicitly referencing a particular data

type. In order to accomplish this, we define some new type classes.

(a) Define a type class Substitutable that specifies that two functions, subst::Subst

a -> a -> a and vars::a -> [String], must be defined for any type a inside this

class. The vars function is meant to return a list of all the variables in a value of type

a.

(b) Within the Substitutable class declaration, define a function solved::Subst a ->

Bool. This function should return True only if the second component of every pair

in its input list has no variables (as determined by the vars function). Otherwise, it

should return False. To avoid generating an Eq a constraint, you may want to use the

null::[a] -> Bool function from the Haskell libraries.

(c) Within the Substitutable class declaration, define a function reduce::Subst a ->

Subst a. This function should take as input a substitution 푠 and collect all the pairs

in 푠 whose second component contains no variables. Call this new list of pairs 푠

′

. It

should then apply 푠

′

to all the second components in 푠, returning the result.

## Problem 3. (10 pts)

(a) Define a type class Unifiable that specifies that a function unify::a -> a -> Maybe

(Subst a) must be defined for any type a inside this class. A type a can only be in the

Unifiable class if it is already in the Eq and Substitutable classes, and this should

be represented in your definition.

(b) Within the Unifiable class declaration, define a function combine::Maybe (Subst a)

-> Maybe (Subst a) -> Maybe (Subst a) that takes two substitutions (one or both

of which might be Nothing) as arguments. If neither one is Nothing, it should combine

them into a single substitution using concatenation. If even one of the arguments is

Nothing, combine should return Nothing.

(c) Modify your definition of the Unify module so that only the values emp, sub, get,

the type constructor Subst, the type classes Substitutable and Unifiable, and the

functions subst, vars, unify, and combine are exported from the module.

2

## Problem 4. (20 pts)

In the module Natural, you will be working with the following data type:

data Natural = Zero | Succ Natural | Var String

(a) Add an instance declaration so that Natural is in the Substitutable class.

(b) Add an instance declaration so that Natural is in the Unifiable class. The unify

function must return a substitution under which the two arguments to unify are equivalent. If the two arguments are syntactically equivalent, unify should return the empty

substitution.

In the module Tree, you will be working with the following data type:

data Tree = Leaf | Node Tree Tree | Var String

(c) Add an instance declaration so that Tree is in the Substitutable class.

(d) Add an instance declaration so that Tree is in the Unifiable class.

## Problem 5. (30 pts)

Within the Unifiable class declaration, define a function resolve::Maybe (Subst a) ->

Maybe (Subst a) that takes a substitution or Nothing as an argument. If its input is

Nothing, it can also return Nothing. If its input is a substitution, however, resolve should

do the following.

(1) Repeatedly apply reduce to the input substitution until no more changes occur when

reduce is applied. You may want to write a helper function to accomplish this. You

may also want to use the nub::Eq a => [a] -> [a] function from the Haskell libraries

to make sure your substitutions do not contain duplicated entries after each reduction.

(2) Once the substitution is stable with respect to reduce, check if it has any conflicts. A

conflict occurs if the substitution contains two pairs (x,u) and (y,v) such that x = y

but u ∕= v. If a conflict exists, resolve should return Nothing.

(3) Check if the substitution is solved by using the solved function. If it is solved, it

should be returned; otherwise, resolve should return Nothing.

You will need to add resolve to the list of functions that you export from the Unify module.

3

## Problem 6. (20 pts)

In the module Equation, equations on a type a are represented in the following way:

data Equation a = a ‘Equals‘ a

(a) Define a function solveEqn::(Unifiable a) => Equation a -> Maybe (Subst a)

that returns the substitution that solves an equation, if possible.

(b) Define a function solveSystem::(Unifiable a) => [Equation a] -> Maybe (Subst

a) that takes a list of equations as an argument, and returns the substitution that solves

the system of equations represented by it, if possible. Be careful: you cannot implement

this correctly if you use your solution from part (a) directly, but the two functions in

parts (a) and (b) may share a helper function.

It is also now possible to define unify on values of type Tree.

(c) Solve the following equations or systems of equations. You are allowed to share your

solutions to these equations, but you may not share any of your Haskell code. For each

equation, define a value in the Tree module that holds its solution (for example, s0

can be the solution for e0, and so on).

e0 = Node (Node (Node (Var “x”) (Var “y”)) (Node (Var “y”) (Var “x”))) (Var “z”)

‘Equals‘

Node (Node (Node Leaf (Var “z”)) (Node Leaf (Var “y”))) (Var “x”)

e1 = let f b 0 = b

f b n = Node (f b (n-1)) (f b (n-1))

in f (Var “x”) 10 ‘Equals‘ f Leaf 13

e2 = [ (Var “z”) ‘Equals‘ Leaf

, Node (Var “y”) Leaf ‘Equals‘ Node Leaf (Var “x”)

, (Var “x”) ‘Equals‘ Node (Var “z”) (Var “z”)

]

4