Center

Page

Web

Wiki

# Tentamen AFP

Swierstra

## 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)
```

• 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