User Tools

Site Tools


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)))
ex-types.txt · Last modified: 2015/10/08 15:20 (external edit)