# Tute (Week 2)

## Table of Contents

## 1 Homework Solutions

Discuss solutions to last week's homework questions.

## 2 Haskell

Consider the Lexer written in last week's code.

### 2.1 Haskell lexical structure

- What is the difference between a
`data`

and a`type`

declaration? - What is the difference between a
*type*and a*data constructor*? List the identifiers in the lexer which represent*type names*, and those which represent data*constructor names*. - Which phase of the compiler would be responsible for distinguishing type and data constructors?

1: A `data`

declaration introduces a new type, for example `Token`

in the lexer. The
`type`

keyword just introduces a new name for an existing type, like `typedef`

in C.
For example, the `String`

type in the standard library is defined merely to be `[Char]`

using a `type`

declaration.

2: A *data constructor* describes a way to create a value of a certain *type*. For example,
the *data constructors* of the *Token* type are:

Kwd :: Keyword -> Token Ident :: String -> Token Times, Minus, Equals, Gt, Lt :: Token LParen, RParen, LBrace, RBrace, Semi :: Token Number :: Int -> Token

3: The *parser* is responsible, as it requires information from the *grammar* of the language
to determine if, for example, `Token`

is a data constructor or a type name, as it is
lexically indistinguishable.

### 2.2 Haskell programming

Currently, the lexer does not handle errors particularly well. Identify some ways in which error reporting could be improved, and how the code ought to be modified to handle errors.

One relatively pain free (and common) way would be to introduce a new constructor of `Token`

to represent invalid words. Information such as what invalid word was encountered, or
where in the source file we are could be added to this token.

data Token = Kwd Keyword | Ident String | Times | Minus | Equals | Gt | Lt | LParen | RParen | LBrace | RBrace | Semi | Number Int | Error Char -- <-- new token deriving (Show) -- all previous cases of lexer, then lexer (e:xs) = Error e : lexer xs

N.B. Adding source positions is quite involved. Whether or not to go that far is up to your tutor. :)

## 3 Inductive Types

Consider the `(++)`

operator in Haskell, which we implemented last week as `append`

.

(++) :: [a] -> [a] -> [a] [] ++ ys = ys (x:xs) ++ ys = x : (xs ++ ys)

- State the formal properties of
*left identity*,*right identity*and*associativity*for`(++)`

. - Try to prove these properties. In some cases, you may
need to perform induction on the structure of lists. The
**base case**of the induction will be for the empty list, and the**inductive case**will be to show your property for a list`(x:xs)`

, assuming the property for the list`xs`

(this assumption is called the*inductive hypothesis*).

1:

[] ++ ys == ys -- left identity xs ++ [] == xs -- right identity (xs ++ (ys ++ zs)) == ((xs ++ ys) ++ zs) -- associativity

2:
Proving left identity is a trivial consequence of the first defining equation of `(++)`

.

For right identity, we want to prove `xs ++ [] == xs`

for all `xs`

.

**Base case**: `xs == []`

, we must show `[] ++ [] == []`

, which follows from the first defining equation.

**Inductive case**: `xs == (x:xs')`

, assuming the inductive hypothesis that:

xs' ++ [] == xs'

We must show that:

(x:xs') ++ [] == (x:xs')

By equational reasoning:

LHS == (x:xs') ++ [] == x:(xs' ++ []) -- Equation 2 == (x:xs') -- Inductive Hypothesis == RHS

Thus right identity is proven by induction on lists.

For associativity, we want to prove `(xs ++ ys) ++ zs == xs ++ (ys ++ zs)`

for all `xs`

, `ys`

and `zs`

. By induction on `xs`

:

**Base case**: `xs == []`

, we must show `([] ++ ys) ++ zs == [] ++ (ys ++ zs)`

. Simplifying
with the first defining equation, both sides become `ys ++ zs`

.

**Inductive case**: `xs == (x:xs')`

. Assuming the inductive hypothesis that:

(xs' ++ ys) ++ zs == xs' ++ (ys ++ zs)

We must show that:

((x:xs') ++ ys) ++ zs == (x:xs') ++ (ys ++ zs)

By equational reasoning:

LHS == ((x:xs') ++ ys) ++ zs == (x:(xs' ++ ys)) ++ zs -- Equation 2 == x:((xs' ++ ys) ++ zs) -- Equation 2 == x:(xs' ++ (ys ++ zs)) -- Inductive Hypothesis == (x:xs') ++ (ys ++ zs) -- Equation 2 (symmetrically) == RHS

Thus associativity is proven by induction on lists.