GPN12:Agda - Mit starken Typen abhängen

aus dem Wiki des Entropia e.V., CCC Karlsruhe
Version vom 4. Juni 2012, 09:34 Uhr von Nomeata (Diskussion | Beiträge)

(Unterschied) ← Nächstältere Version | Aktuelle Version (Unterschied) | Nächstjüngere Version → (Unterschied)
Wechseln zu: Navigation, Suche


Vortrag von nomeata auf der GPN12.

Agda: is it a dependently-typed programming language? Is it a proof-assistant based on intuitionistic type theory? ¯\(°_0)/¯ Dunno, lol.

Programmiersprachen gibt es wie Sand am Meer; wir wollen hier an Stränden sandeln die etwas weiter weg der üblichen touristischen Hochburgen wie C, Java oder PHP sind. Genau gesagt geht es um Agda, was gleichzeitig eine funktionale Programmiersprache (wie Haskell) und ein Theorembeweiser (wie Coq) ist. Der Vortrag ist kein Tutorial, sondern eine Demonstration: nomeata wird einfach den Editor starten und ein kleines Problem live bearbeiten. Dabei wird man sehen wie man mit einem abhängigen Typsystem sich Datentypen definiert, die exakt das darstellen, was man braucht, und wie man damit Ausnahmebehandlungen ersetzt und wie man in Agda selbst die Korrektheit des Programms beweist.

Die Syntax von Agda ist sehr ähnlich der von Haskell und wird nicht besonders ausführlich erklärt. Es ist also nützlich, schon mal Haskell-Code gesehen zu haben. Wer versteht (oder erahnen kann) was dieser Code macht sollte keine Schwierigkeiten haben:

play :: Int -> (Int -> Int) -> (Int -> Int) -> [Int]
play n _ _ | n <= 0 = []
play n p1 p2 = let k = p1 n in n : play (n - k) p2 p1

Mehr Informationen zu Agda: