A Couple Applications

This assign­ment is due May 3 at 11:59 PM. Pull the Github repos­i­tory and start work­ing on Assign­ment4.hs.

Sup­pose we want to com­pute all of the devi­a­tions of a list of num­bers. A devi­a­tion is the dis­tance from the num­ber to the mean of the list, in other words $x - \mu$. Here is naïve approach to the prob­lem.We define our own len func­tion and do not use Haskell’s built-in length because the return type needs to be a Frac­tional for use in aver­age.

len :: Frac­tional b => [a] -> b
len [] = 0
len (_ : xs) = 1 + (len xs)

aver­age :: Frac­tional a => [a] -> a
aver­age xs = (sum xs) / (len xs)

devi­a­tions :: Frac­tional a => [a] -> [a]
devi­a­tions xs = map (sub­tract (aver­age xs)) xs

This is fine, but it tra­verses the list three times. Once for sum, once for len, and once for map. We can improve this sit­u­a­tion by com­put­ing the sum and len simul­ta­ne­ously.

aver­age' :: Frac­tional a => [a] -> (a, a)
aver­age' [] = (0, 0)
aver­age' (x : xs) = (x + sum, 1 + len)
  where (sum, len) = aver­age' xs

aver­age :: Frac­tional a => [a] -> a
aver­age xs = sum / len
  where (sum, len) = aver­age' xs

devi­a­tions :: Frac­tional a => [a] -> [a]
devi­a­tions xs = map (sub­tract (aver­age xs)) xs

Here we only have to trav­ese the list twice. Once for aver­age’ and once for map.

1. Can we do even bet­ter? Can we com­pute this with just a sin­gle tra­ver­sal? If you think it’s pos­si­ble, try to write it. If you think it’s impos­si­ble, why?

2. Read this short post and under­stand how trace com­putes rep­Min. I’ve also posted my own notes on cir­cu­lar pro­gram­ming.

3. Come up with an appro­pri­ate type for devi­a­tions’. We’ve put in a, b, c, d type para­me­ters as a place­holder. You should replace these with the appro­pri­ate types.

4. Write devi­a­tions’ so that devi­a­tions only tra­verses the list once. You should only write devi­a­tions’ and no other recur­sive helper func­tions. Our def­i­n­i­tion of trace is slightly dif­fer­ent than the arti­cle; we don’t use the unnec­es­sary tuple in the input. This is a super­fi­cial dif­fer­ence. (Hint: You may have to use a lazy pat­tern match.)

We talked about the Curry-Howard cor­re­spon­dence and gave the types for sev­eral dif­fer­ent log­i­cal con­cepts.

• Impli­ca­tion cor­re­sponds to func­tion types.

• Dis­junc­tion cor­re­sponds to Either types.

• Con­junc­tion cor­re­sponds to pair types.

• The true propo­si­tion $\top$ cor­re­sponds to the unit type.

A notable omis­sion here is that of log­i­cal nega­tion. Where are our nots? When we learn propo­si­tional logic, we usu­ally take nega­tion as a prim­i­tive notion and impli­ca­tion as a derived notion (by def­i­n­i­tion $P \implies Q$ means $\neg P \vee Q$). How­ever, in the func­tional pro­gram­ming world we’ll take the oppo­site approach, impli­ca­tion (or func­tion types) are prim­i­tive, while nega­tion is derived.

What is the def­i­n­i­tion of not? We’ll define $\neg P$ as $P \implies \bot$ where $\bot$ is some assumed-to-be con­tra­dic­tory propo­si­tion. In Haskell, the equiv­a­lent of $\bot$ is the Void type. A Void type cor­re­sponds to a type with no val­ues, also called an unin­hab­ited type. You can­not make a Void.

Since you can­not make a Void, Haskell will let you con­struct any type if you have a value of type Void using the absurd func­tion. The type of absurd is Void -> a. This is equiv­a­lent to the prin­ci­ple of explo­sion in logic. Assume false and you can prove any­thing.

As an exam­ple, we will show that $(\bot \vee P) \implies P$. Here is the proof.

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

1. Read and under­stand the left­Id exam­ple.

2. Prove $(\neg P \vee Q) \implies (P \implies Q)$ in Haskell by com­plet­ing the body of the impl­Equiv func­tion such that it type­checks.

It turns out that we can­not show the other direc­tion in Haskell! We’ve built up a con­struc­tive logic with­out the law of excluded mid­dle. The con­verse requires this law for its proof. This goes to show that even though we’re able to do a lot of the famil­iar proofs from propo­si­tional logic, some “facts” can­not be shown. Famil­iar things like De Mor­gan’s law or dou­ble nega­tion elim­i­na­tion can­not be proven.

Sub­mit the final source of your project. It should be com­plete. Please include a README that indi­cates how to run it. We will be test­ing it out.

You can still make some tweaks before your pre­sen­ta­tion, but they should be minor.