Note that some tasks may deliberately ask you to look at concepts or libraries that we have not yet discussed in detail. But if you are in doubt about the scope of a task, by all means ask.
Please try to write high-quality code at all times! This means in particular that you should add comments to all parts that are not immediately obvious. Please also pay attention to stylistic issues. The goal is always to submit code that does not just correctly do what was asked for, but also could be committed without further changes to an imaginary company codebase.
Recall the Robot
-DSL from our example session:
data Robot =
Rest
| Go Int
| TurnRight
| TurnLeft
| Seq Robot Robot
| Repeat Int Robot
data RobotSem d = RobotSem
{ rest :: d
, go :: Int -> d
, turnRight :: d
, turnLeft :: d
, seq_ :: d -> d -> d
, repeat_ :: Int -> d -> d
}
foldRobot :: RobotSem d -> Robot -> d
foldRobot sem Rest = rest sem
foldRobot sem (Go n) = go sem n
foldRobot sem TurnRight = turnRight sem
foldRobot sem TurnLeft = turnLeft sem
foldRobot sem (Seq r1 r2) = seq_ sem (foldRobot sem r1) (foldRobot sem r2)
foldRobot sem (Repeat n r) = repeat_ sem n (foldRobot sem r)
Define semantics stepsSem :: RobotSem Int
for calculating the total number of steps
(forwards and backwards) that the robot will go (turning does not count, only going).
Implement a function squareDistance :: Robot -> Natural
thaz calculates the square of the distance (measured in steps)
from the starting point to the end point
for a given command in the Robot
-DSL,
Consider the following simplified DSL for the same robot.
data SimpleRobot =
SimpleRest
| SimpleGo Int SimpleRobot
| SimpleTurnRight SimpleRobot
| SimpleTurnLeft SimpleRobot
Define semantics simpleSem :: RobotSem SimpleRobot
which faithfully translate
a command from the Robot
-DSL to the SimpleRobot
-DSL.
Define the type SimpleRobotSem d
which describes semantics of type d
for the SimpleRobot
-DSL. Also define the corresponding catamorphism
foldSimpleRobot :: SimpleRobotSem d -> SimpleRobot -> d
and
give semantics simpleEnergySem :: SimpleRobotSem Int
for the calculation
of energy consumption.
Make Robot
an instance of the Arbitrary
-class and then write a
property prop_energy_simpleEnergy :: Robot -> Property
which checks that energy consumption for a Robot
-command does not change
when we first translate to a SimpleRobot
-command and calculate energy consumption
afterwards.
Consider the following DSL for describing finite sets of integers:
data FinSet =
Interval Integer Integer
| Union FinSet FinSet
| Intersection FinSet FinSet
Define type FinSetSem d
to describe semantics of type d
for the FinSet
-DSL
and implement the corresponding catamorphism
foldFinSet :: FinSetSem d -> FinSet -> d
.
Implement semantics elemSem :: FinSetSem (Integer -> Bool)
for FinSet
which allow you to decide whether a given integer
is an element of the given set.
Implement semantics minMaxSem :: FinSetSem (Maybe (Integer, Integer))
that allow you to compute minimum and maximum of a FinSet
(or Nothing
if the set is empty).
Define semantics intSetSem :: FinSetSem IntSet
to convert a FinSet
into the
IntSet
(from Data.IntSet
) representing the same set of integers.
Recall the DSL for propositions and related definitions from the lecture:
data Prop =
Var String
| T
| F
| Not Prop
| And Prop Prop
| Or Prop Prop
deriving (Show, Eq)
data PropSem d = PropSem
{ var_ :: String -> d
, t_ :: d
, f_ :: d
, not_ :: d -> d
, and_ :: d -> d -> d
, or_ :: d -> d -> d
}
foldProp :: PropSem d -> Prop -> d
foldProp PropSem{ var_, t_, f_, not_, and_, or_ } = go
where
go (Var s) = var_ s
go T = t_
go F = f_
go (Not p) = not_ $ go p
go (And p q) = and_ (go p) (go q)
go (Or p q) = or_ (go p) (go q)
type Env = String -> Bool
empty :: Env
empty = const False
extend :: String -> Bool -> Env -> Env
extend s b env = \s' -> if s' == s then b else env s'
evalSem :: PropSem (Env -> Bool)
evalSem = PropSem
{ var_ = flip ($)
, t_ = const True
, f_ = const False
, not_ = (not .)
, and_ = \p q env -> p env && q env
, or_ = \p q env -> p env || q env
}
varsSem :: PropSem (Set String)
varsSem = PropSem
{ var_ = S.singleton
, t_ = S.empty
, f_ = S.empty
, not_ = id
, and_ = S.union
, or_ = S.union
}
Implement a function sat :: Prop -> Maybe Env
which checks
whether the given Prop
is satisfiable,
i.e. whether there exists an environment in which the proposition evaluates to True
.
If yes, Just
such an environment is returned.
If no, Nothing
is returned.
It is a well-known fact that instead of using not
, (&&)
and (||)
to construct propositions, just using the single function
nand :: Bool -> Bool -> Bool`
nand x y = not $ x && y
is sufficient.
Consider the following DSL for expressing propositions using the nand
-operation:
data Nand = Var' String | Nand Nand Nand
Define type NandSem d
for semantics of the Nand
-DSL
and the associated catamorphism foldNand :: NandSem d -> Nand -> d
.
Define semantics evalSem' :: NandSem (Env -> Bool)
to evaluate
Nand
-expressions in an environment.
Finally, define semantics nandSem :: PropSem Nand
to convert
from the Prop
-DSL to equivalent propositions in the Nand
-DSL.