Monads and QuickCheck (25 points)
Alternative definitions for
Instead of defining a monad by
, we can also define it in
to avoid confusion with
mmap :: Monad m => (a -> b) -> m a -> m b
join :: Monad m => m (m a) -> m a
join in terms of
bind in terms of
Snoc -lists as Monads
-list is an alternative representation of a (normal) list: a non-empty
-list consists of
the last element of the list, and the rest.
data Snoc a = Nil | Snoc a :< a deriving (Show, Eq)
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 is a
Snoc an instance of the
Monad type class such that the three monad laws are satisfied by giving definitions for the member functions (
- Give the type and the result of the function
test = do x <- listToSnoc [1..5]
- 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)
- 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)
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
\ 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.
- 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
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
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?
- 14 Mar 2011