Biggest Haskell unit in the world

[C T McBride]

On Mon, 25 Jun 2001, Jerzy Karczmarczuk wrote:

JK> I would prefer to read:  
JK> 
JK> A. We teach computer graphics showing all the algorithms in Haskell;

[snip]

JK> E. Artificial Intelligence?

JK> Etc.

JK> It is just a sick dream?

I fear so, but it's not an unusual sick dream. In my version, we also have

F. Logic and Discrete Mathematics: we mediate logic via Haskell,
   emphasising its computation intuition. We find that students
   pathologically terrified by or-elimination respond well to programs
   such as 

> andOverOr :: (a,Either b c) -> Either (a,b) (a,c)
> andOverOr (a,Left b)  = Left  (a,b)
> andOverOr (a,Right c) = Right (a,c)

and

> infix ><

> (><) :: (a -> c) -> (b -> d) -> (a,b) -> (c,d)
> (f >< g) (a,b) = (f a,g b)

   We find it much easier to explain `false implies true' by pointing
   out that there is trivially a function from the empty type to ().

   However, the notation for classic inductive proofs like

> class Nat n

> data O

> data (Nat n) => S n = O | S n

> instance Nat O

> instance (Nat n) => Nat (S n)

> class (Nat n) => Sum n s | n -> s where
>   oneWay   :: (Bool,s) -> (n,S n)
>   otherWay :: (n,S n)  -> (Bool,s)

> instance Sum O O where
>   oneWay   (_,x) = (x, S x)
>   otherWay (x,_) = (True,x)

> instance (Sum n s) => Sum (S n) (Either (S n) s) where
>   oneWay   (True ,Left x) = (x,O)
>   oneWay   (False,Left x) = (O,S x)
>   oneWay   (b,   Right s) = (S >< S) (oneWay (b,s))
>   otherWay (x  ,O)   = (True,Left x)
>   otherWay (O  ,S x) = (False,Left x)
>   otherWay (S x,S y) = (id >< Right) (otherWay (x,y))

   could clearly benefit from syntactic sugar...


But this is the stuff of too much cheese at bedtime. These dreams won't
come true without strong economic pressure...which leads me to this
question, given it's the marking season: which programming language lends
itself most easily to automated analysis of student code? 

Cheers

Conor