GPN12:Agda - Mit starken Typen abhängen

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 Infos zum Vortrag:

• Transskript (PDF-Datei)
• Die Folien der Einführung (interaktives SVG, erstellt mit Sozi)
• Die Folien der Einführung (PDF-Datei)
• Darcs-Repository mit den Quellen von Programm, Vortragstext und Präsentation
• Git-Mirror obiges Repository.

Mehr Informationen zu Agda:

• Die offizielle Homepage
• Gibt es echte Programme in Agda?

GPN12

 Fahrplan |

Aufzeichnungen

GPN12 | Anregungen/Feedback