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