ex-types

# LiP assignment #5

## 1. Rational numbers

Write a record type `num` to represent rational numbers, and the functions:

• `add_num: num → num → num`, that adds two rational numbers.
• `leq_num: num → num → bool`, that compares two rational numbers x, y. It returns `true` if x≤y, otherwise it returns `false`.

Warning: you are not allowed to use floats!

## 2. Card game

Assume we want to model a card game, played with a deck of 40 cards with French suites (spades, hearts, diamonds, clubs). A set of cards if a value of type `deck`, where:

```# type suit = Spades | Hearts | Diamonds | Clubs;;
# type card = Card of int * suit;;
# type deck = Deck of card list;;```

Of course, not all values of type `card` actually represent a card, since cards only make sense when the integer component is comprised between 1 (Ace) and 10 (King).

Write the following functions on decks:

• `deck_complete: deck → bool`, tells whether the given deck is correct and complete, i.e. it is composed by 40 (well-formed) cards, all different.
• `newdeck : unit → deck`, produces a new, complete deck of cards (Note: enumerating all the cards is not permitted.)
• `partition : deck → deck * deck * deck * deck`, partitions the given deck of cards into four decks, which are composed by cards of the same suit.

## 3. Queues

Define a polymorphic type `'a queue` for representing queues, and specify the functions:

• `enqueue: 'a → 'a queue → 'a queue`, that inserts an element in the queue.
• `dequeue: 'a queue → 'a queue`, that removes an element from the queue.
• `isempty: 'a queue → bool`, that returns `true` if the queue is empty.
• `peek: 'a queue → 'a partial`, that peeks the first element from the queue.

## 4. Evaluating arithmetic expressions

Let us extend the syntax of arithmetic expressions, so to also deal with boolean expressions:

```# type exp =
True
| False
| Not of exp
| Or of exp*exp
| And of exp*exp
| Const of int
| Var of string
| Sum of exp * exp
| Sub of exp * exp```

Write the evaluation function for such expressions. Since now the results can either be of type `int` or type `bool`, the return type of the `eval` function should be a variant type, e.g.

```# type result = Bool of bool | Int of int

# let rho = [("x",Int 3); ("y", Bool true)];;

# eval (Sum(Var "x", Const 5)) rho;;
- : result = Int 8```

You shall raise an exception when trying to mix integers with booleans. For instance:

```# eval (Sum(Var "x", Var "y")) rho;;

Exception: Failure "Type mismatch".```

## 5. Simple type checking

Consider the language of logic and arithmetic expressions defined by the following abstract syntax:

```type exp =
Const of int
| Sum of exp * exp
| True
| False
| Not of exp
| And of exp*exp
| Ifthen of exp*exp*exp;;```

Then, consider the following tagged union:

`type t = TInt | TBool | TErr;;`

An expression `e` has type:

• `TInt`, iff
• e = Const v for some v, or
• e = Sum(e1,e2) and both e1 and e2 have type `TInt`, or
• e = Ifthen(e0,e1,e2) and e0 has type `TBool` and both e1 and e2 have type `TInt`
• `TBool` iff
• e = True, or
• e = False, or
• e = Not(e') and e' has type `TBool`, or
• e = And(e1,e2) and both e1 and e2 have type TBool, or
• e = Ifthen(e0,e1,e2) and both e0, e1 and e2 have type `TBool`.
• `TErr`, in all the other cases.

Write a function `typecheck: exp → t` such that `typecheck e` infers the type of `e`.

## 6. Lambda calculus substitutions

Consider the language of λ-terms defined by the following abstract syntax (where x is a variable):

t ::= x | t t | λx. t

For instance, a valid λ-term is (λx.(x (λz.y z))) x.

Write a type `term` to represent λ-terms. Assume that variables are represented as strings.

The free variables fv(t) of a term t are defined inductively a follows:

• fv(x) = {x}
• fv(t t') = fv(t) ∪ fv(t')
• fv(λx. t) = fv(t) \ {x}

For instance, fv((λx.(x (λz.y z))) x) = {x,y}.

Write a function `fv: term → string list` such that `fv t` evaluates to the set (i.e. a list without repetitions) fv(t).

Given two terms t and t', and a variable x, the substitution t{t'/x} is defined inductively as follows:

• x{t'/x} = t'
• y{t'/x} = y, if y≠x
• (t s){t'/x} = t{t'/x} s{t'/x}
• (λx. t){t'/x} = λx. t
• (λy. t){t'/x} = λy. t{t'/x} if y≠x and y∉fv(t')
• otherwise, t{t'/x} is undefined.

For instance, ((λx.(x (λz.y z))) x){y y/x} = (λx.(x (λz.y z))) (y y), while ((λx.(x (λz.y z))) x){z/y} is undefined.

Write a function `subst: string → term → term → term ` such that `subst x t' t` evaluates to t{t'/x} when such substitution is defined, and fails otherwise.

Two λ-terms are alpha-equivalent if they are equal up-to renaming of non-free variables.

For instance, ((λx.(x (λz.y z))) x) and ((λz.(z (λz.y z))) x) are alpha-equivalent, while ((λx.(x (λz.y z))) x) and ((λx.(x (λy.y y))) x) are not (because renaming z as y captures the free occurrence of y).

Write a function `alpha: term → term → bool` such that `alpha t v` evaluates to true iff the λ-terms t and v are alpha-equivalent.

## 7. Binary search trees

A binary search tree is a tree which enjoys the following properties:

• each node has a search “key” and at most two children
• each key is present at most once in the tree
• for any node, the key is greater than the key of every node in the subtree rooted at the left child and less than every key in the subtree rooted at the right child.

Binary search trees are values of the following polymorphic variant type:

`# type 'a bstree = Empty | Node of 'a * 'a bstree * 'a bstree`

The exercise asks for implementing the following functions:

```member : 'a -> 'a bstree -> bool
height : 'a bstree -> int
insert : 'a -> 'a bstree -> 'a bstree
inorder : 'a bstree -> 'a list
sanitycheck : 'a bstree -> bool
maptree : ('a -> 'b) -> 'a bstree -> 'b bstree```

We now briefly discuss the expected behaviour of these functions, with the help of some examples.

The function `member` reports whether or not a key occurs in a tree.

```# member 3 (Node(7, Node(4, Empty, Empty), Empty));;
- : bool = false

# member 4 (Node(7, Node(4, Empty, Empty), Empty));;
- : bool = true```

The funtion `height` computes the length of the longest path in the tree.

```# height Empty;;
- : int = 0

# height (insert 1 (insert 2 (insert 3 (insert 4 Empty))));;
- : int = 4```

The function `insert` inserts a new key into the tree, unless it already exists. The function will construct and return a new binary search tree, which has the inserted key (i.e. there are no side effects)

```# insert 3 (Node(7, Node(4, Empty, Empty), Empty));;
- : bstree = Node (7, Node (4, Node (3, Empty, Empty), Empty), Empty)

# insert 4 (Node(7, Node(4, Empty, Empty), Empty));;
- : bstree = Node (7, Node (4, Empty, Empty), Empty)

# insert 4 Empty;;
- : bstree = Node (4, Empty, Empty)```

The function `inorder` produces a list of the keys visited in a in-order traversal. Given a binary tree, an in-order traversal consists of executing an in-order traversal on the root's left child (if present), then visiting the root, then executing an in-order traversal on the root's right child (if present). Thus, all the left descendents of the root are visited before the root, and the root is visited before any of its right descendents.

```# inorder (insert 4 (insert 8 (insert 2 Empty)));;
- : int list = [2; 4; 8]

# inorder (insert 2 (insert 4 (insert 8 Empty)));;
- : int list = [2; 4; 8]```

The `sanitycheck` function checks if a tree is indeed a binary search tree: that is, if each key is present at most once in the tree, and that for each node, every key in the left child is lower than the key for the node, and every key in the right child is greater. (Hint: can you use `inorder`?)

```# sanitycheck (insert 4 (insert 8 (insert 2 Empty)));;
- : bool = true

# sanitycheck Empty;;
- : bool = true

# sanitycheck (Node (4, Node (4, Empty, Empty), Empty));;
- : bool = false```

The function `maptree` applies a function to each key of a tree.

```# let square x = x * x;;
val square : int -> int = <fun>

# maptree square Node (4, Node (3, Empty, Empty),
Node (7, Node (6, Empty, Empty), Node (9, Empty, Empty)));;
- : bstree = Node (16, Node (9, Empty, Empty),
Node (49, Node (36, Empty, Empty), Node (81, Empty, Empty)))``` 