# A Couple Applications

This assignment is due May 3 at 11:59 PM. Pull the Github repository and start working on `Assignment4.hs`

.

## Deviations Lazily

Suppose we want to compute all of the deviations of a list of numbers. A *deviation* is the distance from the number to the mean of the list, in other words `len`

function and do not use Haskell’s built-in `length`

because the return type needs to be a `Fractional`

for use in `average`

.

len :: Fractional b => [a] -> b len [] = 0 len (_ : xs) = 1 + (len xs) average :: Fractional a => [a] -> a average xs = (sum xs) / (len xs) deviations :: Fractional a => [a] -> [a] deviations xs = map (subtract (average xs)) xs

This is fine, but it traverses the list three times. Once for `sum`

, once for `len`

, and once for `map`

. We can improve this situation by computing the `sum`

and `len`

simultaneously.

average' :: Fractional a => [a] -> (a, a) average' [] = (0, 0) average' (x : xs) = (x + sum, 1 + len) where (sum, len) = average' xs average :: Fractional a => [a] -> a average xs = sum / len where (sum, len) = average' xs deviations :: Fractional a => [a] -> [a] deviations xs = map (subtract (average xs)) xs

Here we only have to travese the list twice. Once for `average’`

and once for `map`

.

Can we do even better? Can we compute this with just a single traversal? If you think it’s possible, try to write it. If you think it’s impossible, why?

Read this short post and understand how

`trace`

computes`repMin`

. I’ve also posted my own notes on circular programming.Come up with an appropriate type for

`deviations’`

. We’ve put in`a, b, c, d`

type parameters as a placeholder. You should replace these with the appropriate types.Write

`deviations’`

so that`deviations`

only traverses the list once. You should only write`deviations’`

and no other recursive helper functions. Our definition of`trace`

is slightly different than the article; we don’t use the unnecessary tuple in the input. This is a superficial difference. (Hint: You may have to use a lazy pattern match.)

## Encoding Negation in Types

We talked about the Curry-Howard correspondence and gave the types for several different logical concepts.

Implication corresponds to function types.

Disjunction corresponds to

`Either`

types.Conjunction corresponds to pair types.

The true proposition

$\top$ corresponds to the unit type.

A notable omission here is that of logical negation. Where are our nots? When we learn propositional logic, we usually take negation as a primitive notion and implication as a derived notion (by definition

What is the definition of not? We’ll define `Void`

type. A `Void`

type corresponds to a type with *no values*, also called an *uninhabited type*. You cannot make a `Void`

.

Since you cannot make a `Void`

, Haskell will let you construct *any* type if you have a value of type `Void`

using the `absurd`

function. The type of `absurd`

is `Void -> a`

. This is equivalent to the principle of explosion in logic. Assume false and you can prove anything.

As an example, we will show that

import Data.Void leftId :: Either Void a -> a leftId (Left x) = absurd x leftId (Right x) = x

Read and understand the

`leftId`

example.Prove

$(\neg P \vee Q) \implies (P \implies Q)$ in Haskell by completing the body of the`implEquiv`

function such that it typechecks.

It turns out that we cannot show the other direction in Haskell! We’ve built up a *constructive logic* without the law of excluded middle. The converse requires this law for its proof. This goes to show that even though we’re able to do a lot of the familiar proofs from propositional logic, some “facts” cannot be shown. Familiar things like De Morgan’s law or double negation elimination cannot be proven.

## Final Project

Submit the final source of your project. It should be complete. Please include a `README`

that indicates how to run it. We will be testing it out.

You can still make some tweaks before your presentation, but they should be minor.