Seminar 2 - Teil II

Dateiinhalt

----------------------------------------------------------------------
--
--  Seminar Theoretische Informatik                         \ \
--  "Funktionale Programmierung mit Haskell"                 \ \ ---
--  Universität Potsdam SS 2014                              / /\ --
--  Tim Richter / Mario Frank                               / /  \
--
--  2: Einfache Typen II
----------------------------------------------------------------------

> module Seminar02_2 where

----------------------------------------------------------------------
-- Typklassen Eq und Ord
----------------------------------------------------------------------

"=" im Gleichheitsschliessen ist mathematische Gleichheitsnotation,
insbesondere ist "alles sich selbst gleich", Funktionen sind gleich,
wenn sie auf allen Werten gleich sind, usw.

Oft benötigt man aber einen Gleichheitstest auf einem Typen, d.h. eine 
(totale, d.h. überall terminierende) Funktion

< (==) :: a -> a -> Bool

Einen solchen Test kann man aber nicht für alle Typen definieren (z.B.
nicht für Funktionen auf Nat).

In Haskell gibt es eine Typklasse aller Typen, für die ein Gleichheits-
test implementiert ist.

< class Eq a where
<   (==),(/=) :: a -> a -> Bool

(==) "sollte" natürlich eine Äquivalenzrelation definieren,
aber es könnte auch x == y = False definiert werden.

Auch selbstdefinierte Typen können zu "instances" von Typklassen gemacht
werden, z.B.

> data AN = MarcUwe | Känguru | Krapottke | FW
>
> instance Eq AN where
>   x == y = True

Es genügt, (==) oder (/=) zu definieren, für die jeweils andere Funktion
gibt es die Defaultdefinitionen

< x /= y = not ( x == y )
< x == y = not ( x /= y )

Wieder gibt es die "semantische" oder "moralische" Verpflichtung,
  x == y  =  not ( x /= y )
auch dann zu haben, wenn man sowohl (==) als auch (/=) implementiert,
aber Haskell kann dies nicht erzwingen.

Es gibt darüberhinaus die Typklasse Ord

< class Eq a => Ord a where
<  (<),(<=),(>=),(>) :: a -> a -> Bool
<  compare :: a -> a -> Ordering

Hier ist

< data Ordering = LT | EQ | GT

und Definition von compare reicht wieder aus.

> instance Ord AN where
>   compare x y = EQ

Für viele Typen kann Haskell automatisch Typklasseninstanzen
ableiten:

> data Triangletype = Failure | Isosceles | Equilateral | Scalene 
>     deriving (Eq, Ord, Show)

Die meisten builtin Types (z.B. Int) sind ohnehin in Eq, Ord, ...

(==),(<=) etc. sind nützlich, um Funktionen mit Hilfe von sogenannten
"guards" zu definieren:

> analyse :: (Int,Int,Int) -> Triangletype
> analyse (x,y,z) | x + y <= z           = Failure
>                 | x == z               = Equilateral
>                 | (x == y) || (y == z) = Isosceles
>                 | otherwise            = Scalene

Es gibt hier nur ein pattern, alle Tripel aus (Int,Int,Int) (bis auf 
undefined, (undefined,2,3) usw.) matchen auf dieses pattern.

Die "guards" sind Boolsche Ausdrücke, werden wie pattern von oben nach 
unten ausgewertet, falls True, wird zur rechten Seite von "=" reduziert.
otherwise (= True) am Ende ist der default Fall.

----------------------------------------------------------------------
-- Enumerations
----------------------------------------------------------------------

< class Enum a where
<   succ :: a -> a
<   pred :: a -> a
<   toEnum :: Int -> a
<   fromEnum :: a -> Int
<   ...

Typen, die "durchgezählt" werden können. Ausreichend zur Instanziierung
sind die Definitionen von toEnum und fromEnum. Für Charaktere kennt man
in vielen Programmiersprachen Funktionen ord und chr, die zwischen einem
Zeichen und seinem ASCII-Code übersetzen. In Haskell sind diese nicht
vordefiniert, Char ist aber in Enum und fromEnum und toEnum machen genau
die Arbeit von ord und chr

> ord :: Char -> Int
> ord = fromEnum
>
> chr :: Int -> Char
> chr = toEnum

Man erwartet natürlich von Implementationen, dass sie

  toEnum ( fromEnum x) = x

erfüllen. Dieses "Gesetz" kann Haskell aber nicht erzwingen,
der Programmierer muss selbst aufpassen.

Auch hier gibt es "deriving" für viele Typen, z.B.

> data Wochentag = Mo | Di | Mi | Do | Fr | Sa | So
>   deriving (Eq, Ord, Enum, Bounded, Show)

Bounded ist eine weitere Typklasse, die

< minBound, maxBound :: a

definiert.

Übung: Definieren Sie Funktionen unter Benutzung von fromEnum und/oder
toEnum

< arbeitstag, wochenende :: Wochentag -> Bool

----------------------------------------------------------------------
-- Tupel
----------------------------------------------------------------------

Wir hatten Tupel schon benutzt ((Int,Int,Int)) usw. (,) ist syntactic 
sugar, aber ansonsten ist (a,b) ganz analog zu

> data Pair a b = MkPair a b

Zwei Typparameter, a und b, sie können verschieden sein!
Der Datentyp hat den Datenkonstruktor

< MkPair :: a -> b -> Pair a b

Typkonstruktoren und Datenkontruktoren dürfen denselben Namen benutzen!
Aber: zwei Datenkonstruktoren (auch verschiedener Typen) dürfen nicht 
gleich heissen!

Standardfunktionen sind die Projektionen

< fst :: (a,b) -> a
< fst (x,y) = x
<
< snd :: (a,b) -> b
< snd (x,y) = y

Da Konstruktoren immer non-strict sind, sind 
  (undefined,undefined) und undefined verschieden

Übung: Schreiben Sie eine Funktion

< test :: (Int,Int) -> Bool

die sich auf diesen beiden Werten unterschiedlich verhält!

Für das Gleichheitsschliessen und die "algebra of programming" wichtige 
higher order functions für (,) sind:

> pair :: (a->b,a->c) -> a -> (b,c)
> pair (f,g) x = (f x, g x)

> cross :: (a->b,c->d) -> (a,c) -> (b,d)
> cross (f,g) = pair (f . fst, g . snd)

Leicht beweist man folgende Gesetze:

 1)  fst . pair (f, g)        =  f
 2)  snd . pair (f, g)        =  g
 3)  pair (f, g) . h          =  pair (f.h,g.h)
 4)  cross (f,g) . pair (h,k) =  pair (f.h,g.k)

Zur Illustration der Beweis für 4) unter Benutzung von 1),2) und 3)

  cross (f,g) . pair (h,k)
  =  {def cross}
  pair (f.fst, g.snd) . pair (h,k)
  =  { 3) }
  pair (f.fst.pair(h,k), g.snd.pair(h,k))
  =  { 1) und 2) }
  pair (f.h,g.k)

----------------------------------------------------------------------
-- Either
----------------------------------------------------------------------

< data Either a b = Left a | Right b

Hier haben wir zwei Konstruktoren:

<   Left   :: a -> Either a b
<   Right  :: b -> Either a b

Wichtige higher order functions:

> scase :: (a->c,b->c) -> Either a b -> c
> scase (f,g) (Left x)   = f x
> scase (f,g) (Right y)  = g y

> plus :: (a->b,c->d) -> Either a c -> Either b d
> plus (f,g) = scase (Left . f, Right . g)

Either a b ist "dual" zu (a,b) und es gelten für scase und plus
analoge Gesetze wie für cross und pair:

i)   scase (f,g) . Left      = f
ii)  scase (f,g) . Right     = g
iii) h . scase (f,g)         = scase (h.f,h.g)
iv)  scase (f,g) . plus(h,k) = scase (f.h,g.k)

Übung: Vergleichen Sie mit 1)-4) oben! Beweisen Sie iv) unter
Benutzung von i)-iii)!

Bemerkung: In Birds Buch heisst die Funktion scase "case". Das 
kollidiert mit dem ghc-Schlüsselwort "case".