COMP[39]161 Concepts of Programming Languages
Semester 2, 2018

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

  1. What is the difference between a data and a type declaration?
  2. 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.
  3. 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)
  1. State the formal properties of left identity, right identity and associativity for (++).
  2. 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.

2018-11-16 Fri 19:37

Announcements RSS