Tentamen AFP

Monads and QuickCheck (25 points)

Alternative definitions for Monad operations.

Instead of defining a monad by bind (>>=)and return, we can also define it in terms of map (hereafter called mmap to avoid confusion with map from the Prelude), join, and return.

mmap  :: Monad m => (a -> b) -> m a -> m b
join  :: Monad m => m (m a) -> m a

• Define mmap and join in terms of bind (>>=) and return, and
• define bind in terms of mmap, join, and return.

Snoc -lists as Monads

A Snoc -list is an alternative representation of a (normal) list: a non-empty Snoc -list consists of the last element of the list, and the rest.

data Snoc a = Nil | Snoc a :< a deriving (Show, Eq)

• Define listToSnoc, such that listToSnoc [1..5] returns ((((Nil :< 1) :< 2) :< 3) :< 4) :< 5. Use higher-order functions if possible.

<++

• Define the operator (<++) :: Snoc a -> Snoc a -> Snoc a for concatenating two Snoc -lists.

Snoc is a Monad

• Make Snoc an instance of the Monad type class such that the three monad laws are satisfied by giving definitions for the member functions (>>=) and return.

The function test

• Give the type and the result of the function test.

test = do  x <- listToSnoc [1..5]
           return (x*x)

Monad laws

• Prove that the first two monad laws hold for a |Snoc|-list. Use equational reasoning.

return x >>= f   is equivalent to  f x (left-identity)
m >>= return      is equivalent to m   (right-identity)

Quickcheck

• Give a QuickCheck property to check that also the third monad law holds.

(m >>= f) >>= g  is equivalent to m >>= (\x -> f x >>= g)  (associativity)

• Indicate precisely how this property can be validated by the QuickCheck system, and make sure that QuickCheck is able to generate random Snoc -lists (with an appropriate distribution of test cases). Do not forget to give the type signature as this is required by the  =QuickCheck system.

De-Bruijn numbering (40 points)

Alfa conversion

When we substitute lambda-terms when doing beta-reduction without taking proper precautions we may get name clashes.

• Give as an example how things can go wrong if we do not use alfa-conversion (i.e. systematically rename lambda-bound names).

De Bruijn numbering

The Dutch logician De Bruijn proposed a representation of lambda-terms in which each variable is replaced by a number which tells how many lambda-hops away its binding occurrence is. So the lambda expression \ x -> \y -> y is represented by \_  -> \_ -> 0 and \ x -> \y -> x is represented by \_  -> \_ -> 1, etc. Note that the names which were introduced originally have disappeared. The identifiers have been replaced by a number telling how many static levels upwards from the used position the corresponding parameter binding can be found. We give the data types:

data Lam = LVar String | LApp Lam Lam | Lambda String Lam

data DBLam = DBVar Int | DBApp Lam Lam | DBLamda  Lam

• Write a function compile :: Lam -> DBLam which maps the first to the second.
• Show with a few examples that your compiler works as expected.

Evaluation

• Write a function normDB :: DBLam -> DBLam, which normalises a DBLam to a normal form, if it exists. Make sure that you keep your numbering scheme correct!

runST (10 points)

• Explain, in your own words, why the type of runST makes sure that no unsafe access is given to the internals of the maintained state. Why is it not a problem if references to this internal state escape.

Idiomatic (25 points)

We define the class Idiomatic as follows:

data Stop = Stop
stop = Stop

start :: forall a g. (Idiomatic f g) => f -> g
start f = idiomatic (pure f)

class Idiomatic f g | g -> f  where
    idiomatic :: Parser f -> g
instance  Idiomatic  x (Stop -> Parser x) where
    idiomatic ix Stop = ix
instance Idiomatic f g => Idiomatic (a -> f) (Parser a -> g) where
    idiomatic isf is = idiomatic (isf <*> is)

so we can omit the sequencing <*> operators from our parsers. Note that we have left out the i parameter, since we have specialised things here for parsers.

An example of a somewhat extended and more specialised approach can be found here. The underlying ideas were explained in the exercise of the paper Applicative programming with effects, and the solution in the code above is hinted at (at the bottom of page 4).

How does this work?

• Explain in your own wording the working of this code using e.g. the definition of the function eval at the bottom op this same page. Which instances are being passed. Why are the functional dependencies important?

Extending the collection of instances

• What instance should be aded to the code on the page Idioms, such that the example there could have been written as: run (iI (+) '(' one "+"  one ')' Ii) "(2+3)" in a context where one :: Int, i.e. by replacing the pNatural by a integer value?

-- DoaitseSwierstra - 14 Mar 2011