GPN12:Agda - Mit starken Typen abhängen: Unterschied zwischen den Versionen

aus dem Wiki des Entropia e.V., CCC Karlsruhe
Keine Bearbeitungszusammenfassung
(mirror git repo)
 
(Eine dazwischenliegende Version desselben Benutzers wird nicht angezeigt)
Zeile 22: Zeile 22:
* [[Media:AgdaTalk-Slides.pdf|Die Folien der Einführung]] (PDF-Datei)
* [[Media:AgdaTalk-Slides.pdf|Die Folien der Einführung]] (PDF-Datei)
* [http://darcs.nomeata.de/gpn12-agda-talk/ Darcs-Repository] mit den Quellen von Programm, Vortragstext und Präsentation
* [http://darcs.nomeata.de/gpn12-agda-talk/ Darcs-Repository] mit den Quellen von Programm, Vortragstext und Präsentation
* [http://git.nomeata.de/?p=darcs-mirror-gpn12-agda-talk.git;a=summary Git-Mirror] obiges Repository.
* [http://git.nomeata.de/?p=darcs-mirror-gpn12-agda-talk.git;a=summary Git-Mirror] obiges Repository. ([[Media:Darcs-mirror-gpn12-agda-talk.tar.gz|Stand 06.07.2012]])


Mehr Informationen zu Agda:
Mehr Informationen zu Agda:
Zeile 28: Zeile 28:
* [http://stackoverflow.com/questions/10931316/real-programs-written-in-agda Gibt es echte Programme in Agda?]
* [http://stackoverflow.com/questions/10931316/real-programs-written-in-agda Gibt es echte Programme in Agda?]


[[Kategorie:GPN12]]
{{Navigationsleiste GPN12:Vorträge}}
[[Kategorie:Vorträge]]
{{Navigationsleiste GPN12}}

Aktuelle Version vom 6. Juli 2012, 10:53 Uhr


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:

Mehr Informationen zu Agda: