Einführung - 10.04.2014
Tim Richter
intro.lhs
—
LHS source code,
14Kb
Dateiinhalt
----------------------------------------------------------------------
--
-- Seminar Theoretische Informatik \ \
-- "Funktionale Programmierung mit Haskell" \ \ ---
-- Universität Potsdam SS 2014 / /\ --
-- Tim Richter / Mario Frank / / \
--
----------------------------------------------------------------------
"There are two ways of constructing a software design:
One way is to make it so simple that there are obviously no deficiencies,
and the other way is to make it so complicated that there are no
obvious deficiencies.
The first method is far more difficult." Tony Hoare
-------------------------------------------------------------------------
-- Haskell
-------------------------------------------------------------------------
lazy (non-strict, "call by need"), (polymorphically) statically typed
purely functional programming language
benannt nach Haskell Brooks Curry (1900-1982)
entwickelt ab 1987 vom "Haskell Committee"
Wurzeln: Lambda-Kalkül, ISWIM, LISP, Scheme, ML, Miranda...
Ziele: geeignet für Lehre, Forschung und Anwendungen jeder Größe
Status: Sprachstandard momentan "Haskell 2010"
nach wie vor in der Forschung verwendet
mehr und mehr aber auch in Anwendungen
"Hackage has over 5000 packages written by over 1000 people"
zur Geschichte: Hudak, Hughes, Peyton Jones, Wadler:
"A History of Haskell - Being Lazy with Class"
Literatur
Richard Bird: "Introduction to Functional Programming using Haskell",
2nd edition, Prentice Hall 1998
5 Exemplare in der Bibliothek, werden gerade "eingearbeitet"
Graham Hutton: "Programming in Haskell", CUP 2007
Simon Thompson: "Haskell: the craft of functional programming",
Addison Wesley, 2011
einige Exemplare im Lesesaal
Haskell platform: http://www.haskell.org/platform/
beinhaltet
ghc - Glasgow Haskell Compiler
ghci - Haskell REPL
cabal - Paketmanager
für Linux, MacOs und Windows verfügbar, unter Debian/Ubuntu z.B. mit
apt-get install haskell-platform
Online ressourcen, tutorials, blogs etc: Starten Sie beim
Haskellwiki http://www.haskell.org/
Nützlich insbesondere:
School of Haskell
Hoogle
"Learn you a Haskell for great good"
"Real world Haskell"
---------------------------------------------------------------------
-- Dieses Seminar
---------------------------------------------------------------------
Wir arbeiten nach Bird's Buch. Teilnehmer
- stellen jeweils zu zweit in einer Sitzung (1 1/2 h) ca. ein
Kapitel des Buches vor
ungefähr 1 Woche vor dem Termin *Konsultation* mit vorbereitetem
literate Haskell Skript
Skript wird *zwei Tage vor dem Vortrag* abgegeben und zum Download
bereitgestellt
- schicken Lösungen für die Übungsaufgaben termingerecht an
tim@cs.uni-potsdam.de *und* eladrion@cs.uni-potsdam.de
- bearbeiten ein kleines Projekt in Haskell:
Aufgabenstellungen gibt es Mitte Mai, Abgabe 31.07.
in Form eines lhs-Skripts mit Darstellung der Spezifikation,
Programmtransformationen (ggf. mit Beweisen von Eigenschaften)
und der lauffähigen Implementation.
Ideen und Vorschläge sind willkommen.
Für die Note werden die Übungsaufgaben zu 20%, Vortrag und Projekt
zu je 40% gewertet.
Vorläufiger Ablaufplan Ch.3 -"-
08.05. Listen Ch.4
Termin Thema Literatur Vortragende(r)
10.04. Einführung Bird Ch.1 Richter
17.04. Einfache Typen Ch.2 -"-
24.04. Zahlen Ch.3 -"-
08.05. Listen Ch.4 44S. Matthias Seidel, Olaf Gühlke
15.05. Listen 2
22.05. Übung
05.06. Bäume (+Bsp.Klassenliste) Ch.6(+5) 35+8S. Hendrik Geßner, Manuel Zedel
12.06. Effizienz (+Bsp.Kalender) Ch.7(+5) 30+16S. Tim Richter
19.06. * Übung
26.06. Abstrakte Datentypen Ch.8 42S. Vitaly Stanchits
03.07. Monaden/Parsing Ch.10+11 46S. Fabrice Raddatz, Johannes Wutzke
10.07. Minibeweiser Ch.12 Henrik Jürges, Philip Ullrich
17.07. * Übung
-------------------------------------------------------------------
-- Erste Schritte mit ghci
-------------------------------------------------------------------
ghci funktioniert wie ein Taschenrechner:
read - eval - print - loop (REPL)
Nach Start von ghci hat man ein prompt
Prelude>
Das Haskell-"Prelude" ist ein Standard-Modul, das ghci beim Start
automatisch lädt. Built-in oder im "Prelude" definiert sind:
- Basistypen Bool, Integer, Int, Float, Double, Char (z.B. 'x'), ...
- Grundlegende Typkonstruktoren: [a] (Listen von Elementen des Typs a),
(a,b) (Paare, deren 1.Komponente vom Typ a und deren 2.Komponente vom
Typ b ist), ...
- Grundlegende Funktionen und Operatoren wie (+), (-), (*),
"if ... then ... else ...", Listenverkettung (++),
fst :: (a,b) -> a, snd :: (a,b) -> b usw.
Probieren Sie das Kommando:
Prelude> :browse Prelude
Man kann nun Ausdrücke eingeben, nach <Enter>
- prüft ghci, ob der gegebene Ausdruck typkorrekt ist (type checking),
- wenn nicht, gibt ghci eine mehr oder minder informative Fehlermeldung.
- Ist der Ausdruck typkorrekt, wird er durch Anwendung der Definitionen
der enthaltenen Operatoren und Funktionen reduziert oder "evaluiert".
Falls keine weitere Reduktion möglich ist, wird die erreichte
Representation ( die "Normalform" oder der "Wert" des Ausdrucks)
ausgegeben:
Prelude> (3 + 4) * 6
42
( Es gibt auch Ausdrücke, die immer weiter reduziert werden können, siehe z.B.
infinity unten.
Man kann Ausdrücken Namen geben, z.B.
Prelude> let a = (3 + 4) * (2 + 6)
Wenn der Ausdruck auf der rechten Seite des "=" typkorrekt ist, wird a
als Name für diesen Ausdruck der lokalen Auswertungsumgebung (environment)
hinzugefügt. ":show bindings" zeigt letztere:
Prelude> :show bindings
it :: Integer = 42
a :: Integer = _
"a" taucht hier als Name eines Ausdrucks vom Typ Integer auf
(type checking war also erfolgreich), ist aber bisher nicht evaluiert
worden ( = _ ).
"it" ist ein Name für den zuletzt erfolgreich evaluierten Ausdruck.
Prelude> if True then 5 else a
5
Prelude> :show bindings
a :: Integer = _
it :: Integer = 5
Noch immer wurde a nicht ausgewertet!
Prelude> if False then 5 else a
56
Prelude> :show bindings
a :: Integer = 56
it :: Integer = 56
Jetzt hat a den Wert 56.
Wir können auch Datentypen direkt in ghci deklarieren:
Prelude> data Nat = O | S Nat deriving Show
Durch diese Deklaration wird angegeben, dass
- Nat ein Typ
- O :: Nat
- für jedes n :: Nat auch (S n) :: Nat
ist. Nat ist ein "Typkonstruktor", O und S sind "Datenkonstruktoren".
Konstruktoren *müssen* in Haskell immer mit einem Grossbuchstaben
beginnen!
Nat soll die natürlichen Zahlen beschreiben: O steht für die Null
und (S n) für den Nachfolger von n. Nat enthält also jedenfalls
O, S O, S (S O), S (S (S O)),...
Aber nicht nur diese! Folgende Definition ist in Haskell ohne
Problem möglich:
Prelude> let infinity = S infinity
Prelude> :type infinty
infinity :: Nat
Wie wird dieser Ausdruck ausgewertet?
infinity
= { Definition infinity }
S infinity
= { Definition infinity }
S (S infinity)
= ...
Die Auswertung (Evaluation) wird also nicht fertig. Versuchen Sie
in ghci:
Prelude> infinity
Ctrl-C bricht ab!
Dass infinity nicht vollständig evaluiert werden kann, verhindert
aber nicht, damit zu rechnen. Implementiert man z.B. (<) für Nat so,
dass
O < S n = True
für beliebiges n :: Nat (siehe Übungsaufgaben), dann ist
O < infinity
= { Definition infinity }
O < S infinity
= { Definition (<)}
True
Diese Art, schrittweise Umformungen von Ausdrücken aufzuschreiben,
und dabei in { } eine Begründung für die Gleichheit zweier Ausdrücke
anzugeben, heisst "Gleichheitsschliessen" (equational reasoning).
Equational reasoning wird in diesem Seminar eine grosse Rolle spielen.
Nützliche ghci Kommandos:
:load <filename> Skript laden
:reload Skript neu laden
:type <expr> Typ eines Ausdrucks
:module [+/-] <mod> Modul zur Auswertungsumgebung hinzufügen
oder aus ihr entfernen
:browse <modul> Definitionen in Modul auflisten
:h Hilfe
--------------------------------------------------------------------
-- Skripte
--------------------------------------------------------------------
Lokale Bindungen mit "let.." sind nett, aber natürlich möchte man
Deklarationen und Definitionen auch in Dateien schreiben und aus
Dateien lesen können. Für solche Haskell-Skripte gibt es verschiedene
Stile, wir verwenden "Literate Haskell" im "Bird-Style": Codezeilen
beginnen mit "> ", alles andere ist Kommentar, die Dateiendung ist lhs.
> module Intro where
> import Data.Complex
>
> intSq :: Integer -> Integer
> intSq x = x * x
>
> intMin :: (Integer,Integer) -> Integer
> intMin (x,y) = if (x < y) then x else y
>
> square :: Complex Double -> Complex Double
> square z = z * z
Das Skript definiert das Modul "Intro", importiert das Modul Data.Complex
(das mit ghc kommt und Datentypen komplexer Zahlen definiert),
und definiert drei Funktionen. Mehr zu Modulen und imports später.
Complex Double hat Elemente der Form (a :+ b), wobei a und b vom
Typ Double (Floating point Zahlen mit doppelter Präzision) sind.
In den Definitionen von intSq und square beachte man die Überladung
des Multiplikationsoperators "*" !
Wir laden das Skript in unsere ghci-Session:
Prelude> :l intro.lhs
[1 of 1] Compiling Intro ( intro.lhs, interpreted )
Ok, modules loaded: Intro.
*Intro>
--------------------------------------------------------------------
-- Beispiel: Mandelbrotmenge
--------------------------------------------------------------------
Wir wollen zum Abschluss eine (ASCII-, also lächerlich grobe)
Darstellung der Mandelbrotmenge in unserer ghci-Session anzeigen.
Die Mandelbrotmenge ist die Teilmenge derjenigen komplexen Zahlen c,
für die die rekursiv definierte Folge
z_(c,0) = 0
z_(c,(n+1)) = z_(c,n) * z_(c,n) + c
komplexer Zahlen beschränkt ist. D.h. es gibt eine (evtl. von c
abhängige) reelle Zahl b_c, die grösser ist als der Betrag jedes
Folgengliedes.
Eine für uns ausreichende Approximation ist die
Menge der Zahlen c, für die
|z_(c,1000)| < 1000.0
ist.
Definieren wir zunächst die Folge
> mbiter :: Complex Double -> Int -> Complex Double
> mbiter c 0 = 0
> mbiter c n = square (mbiter c (n-1)) + c
und nun unsere Approximation der Mandelbrotmenge als Funktion
von den komplexen Zahlen in den Typ der Wahrheitswerte, Bool,
der im Prelude durch
data Bool = False | True
definiert ist:
> mb :: Complex Double -> Bool
> mb c = magnitude (mbiter c 1000) < 1000.0
mb ist eine Art "charakteristische Funktion". Zur Darstellung
definieren wir eine Funktion
> mbch :: Complex Double -> Char
> mbch = (\b -> if b then '*' else ' ') . mb
In Klammern steht ein Lambda-Ausdruck: Eine unbenannte Funktion
vom Typ (Bool -> Char), die True nach '*' und False nach ' ' abbildet.
Wir wollen mbch auf komplexe Zahlen anwenden, die gitterartig
aus einem geeigneten Bereich der komplexen Ebene genommen werden.
Wir stellen das Gitter als Liste von Listen komplexer Zahlen dar:
> cgrid :: [[Complex Double]]
> cgrid = [[ (minr + dr*u) :+ (maxi - di*v) | u <- [0..w]]
> | v <- [0..h]] where
> minr = -2.0
> maxr = 1.0
> mini = -1.0
> maxi = 1.0
> w = 80
> h = 30
> dr = (maxr - minr) / w
> di = (maxi - mini) / h
Die verwendete "list comprehension" Notation ist hoffentlich
intuitiv verständlich, im Kapitel 4 wird sie genauer erklärt.
Nun "mappen" wir mbch über dieses Gitter und erhalten eine Liste
von Listen von Charakteren, [[Char]]. Für den Typ [Char] gibt es
das Typsynonym String, wir erhalten also eine Liste von Strings
> mandelbrot :: [String]
> mandelbrot = map (map mbch) cgrid
die wir in ghci anzeigen können
*Intro> sequence_ ( map putStrLn mandelbrot )
*
*****
*****
***
** *************
***********************
**********************
**************************
*****************************
* *****************************
********* *****************************
*********** ******************************
******************************************
*************************************************************
******************************************
*********** ******************************
********* *****************************
* *****************************
*****************************
**************************
**********************
***********************
** *************
***
*****
*****
*
