Hi *,
am Sonntag, 30. November 2014 treffen wir uns um 12:00 in India King
für unser Hackathon. Bringt eure Laptops!
Themen:
- Agda: wir machen weiter mit den Agda-Tutorial:
http://oxij.org/note/BrutalDepTypes/
oder
- Buch: Homotopy Type Theory (HoTT)
oder
- wir hacken ein bisschen an Android rum, um später ein Haskell DSL zu
schreiben welches auf Android Apps runterkompiliert
-- BERICHT --
16. November 2014
- über Agda gesprochen und darüber, was Theorem Prover sind
- wofür die gut sind
- Haskell installiert
- Agda installiert
- Emacs installiert und für Agda konfiguriert
-- ANFAHRT --
Wir treffen uns in India King, Landsbergerstr. 491.
Webseite: http://www.indiaking.de
Karte: https://goo.gl/maps/5g9m6
Anfahrtmöglichkeiten:
- S-Bahn nach Pasing nehmen (alle außer S1, S2 und S7) und dann Tram
19 nach Offenbachstraße (2 Haltestellen)
- Tram 19 von Hauptbahnhof richtung Pasing nehmen bis Offenbachstraße
- Bus 130 oder 131 zum Knie nehmen und dort in die Tram 19 nach Pasing
umsteigen, bis Offenbachstraße
- Bus 160 oder 162 nach Offenbachstraße
India King befindet sich genau gegenüber der Tramhaltestelle.
Twitter: https://twitter.com/Haskell_hackers
Web: http://haskell-hackathon.no-ip.org
English: http://haskell-hackathon.no-ip.org/index_en.html
Dear all,
next week, on Wednesday, 26th of November, our monthly Munich Haskell Meeting
will take place again at Cafe Puck at 19:30 CET. For details see here:
http://www.haskell-munich.de/dates
Since Heinrich is not around much in Munich anymore, I have taken over
organizing our Haskell meeting. The website will be updated soon.
For the meantime, if you plan to join, please add yourself to
this dudle so we can reserve enough seats:
https://dudle.inf.tu-dresden.de/haskell-munich-nov-2014/
Everybody is welcome!
Looking forward to see you,
--
Christian Neukirchen <chneukirchen(a)gmail.com> http://chneukirchen.org
Hi *,
am Sonntag, 23. November 2014 treffen wir uns um 16:00 in India King
für unser Hackathon. Bringt eure Laptops!
Themen:
- Agda: wir versuchen ein einfaches Programm zu schreiben
oder
- Buch: Homotopy Type Theory (HoTT)
oder
- wir hacken ein bisschen an Android rum, um später ein Haskell DSL zu
schreiben welches auf Android Apps runterkompiliert
-- BERICHT --
5. November 2014
- wir haben Agda 2.4.2 installiert. Es hat ein paar Probleme auf Grund
von cabal gegeben, die konnte man aber lösen indem man --constraint
benutzt hat.
- man kann Agda übrigens auch im sandbox installieren
- einer von uns hat zuvor Agda 2.3.2 aus einen .deb installiert. Das
hat auch einige haskell-libraries zurückgelassen; nach deren
entfernung waren die noch im ghc index vorhanden, aber kaputt (.so
Dateien nicht vorhanden). Das haben wir mit cabal install --reinstall
gelöst.
- man muss zuerst das agda-mode Plugin für Emacs installieren: agda-mode setup
- danach muss man die stlib runterladen:
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary
- und das src von stdlib Unterverzeichnis in Emacs als include-path
für agda2-mode hinterlegen: in Emacs über M-x customize-group RET
agda2 RET
- wir haben ein einfaches Tutorial angefangen:
http://www.stephendiehl.com/posts/agda.html
- es gibt auch "agda summer school":
https://github.com/UlfNorell/agda-summer-school/ -- die benutzte
library ("agda prelude") ist aber mit der stdlib von Agda inkompatibel
- wir haben über online-foren für HoTT gesprochen:
"hott amateurs": https://groups.google.com/forum/#!forum/hott-amateurs
das offizielle Forum für HoTT:
https://groups.google.com/forum/#!forum/homotopytypetheory
IRC: ##hott auf Freenode
-- ANFAHRT --
Wir treffen uns in India King, Landsbergerstr. 491.
Webseite: http://www.indiaking.de
Karte: https://goo.gl/maps/5g9m6
Anfahrtmöglichkeiten:
- S-Bahn nach Pasing nehmen (alle außer S1, S2 und S7) und dann Tram
19 nach Offenbachstraße (2 Haltestellen)
- Tram 19 von Hauptbahnhof richtung Pasing nehmen bis Offenbachstraße
- Bus 130 oder 131 zum Knie nehmen und dort in die Tram 19 nach Pasing
umsteigen, bis Offenbachstraße
- Bus 160 oder 162 nach Offenbachstraße
India King befindet sich genau gegenüber der Tramhaltestelle.
Twitter: https://twitter.com/Haskell_hackers
Web: http://haskell-hackathon.no-ip.org
English: http://haskell-hackathon.no-ip.org/index_en.html
Hi *,
am Sonntag, 16. November 2014 treffen wir uns um 16:00 in India King
für unser Hackathon. Bringt eure Laptops!
Themen:
- Agda: wir versuchen ein einfaches Programm zu schreiben
oder
- Buch: Homotopy Type Theory (HoTT)
oder
- wir hacken ein bisschen an Android rum, um später ein Haskell DSL zu
schreiben welches auf Android Apps runterkompiliert
-- BERICHT --
2. November 2014
- wir haben HoTT gelesen
- wir haben uns theorem prover angeschaut und vergliechen: Agda, Coq,
Isabelle/HOL, Idris.
- Nur Agda und Coq sind für HoTT nutzbar
- Idris und Isabelle/HOL sind aber für viele Sachen viel mehr praktisch
-- ANFAHRT --
Wir treffen uns in India King, Landsbergerstr. 491.
Webseite: http://www.indiaking.de
Karte: https://goo.gl/maps/5g9m6
Anfahrtmöglichkeiten:
- S-Bahn nach Pasing nehmen (alle außer S1, S2 und S7) und dann Tram
19 nach Offenbachstraße (2 Haltestellen)
- Tram 19 von Hauptbahnhof richtung Pasing nehmen bis Offenbachstraße
- Bus 130 oder 131 zum Knie nehmen und dort in die Tram 19 nach Pasing
umsteigen, bis Offenbachstraße
- Bus 160 oder 162 nach Offenbachstraße
India King befindet sich genau gegenüber der Tramhaltestelle.
Twitter: https://twitter.com/Haskell_hackers
Web: http://haskell-hackathon.no-ip.org
English: http://haskell-hackathon.no-ip.org/index_en.html
Hi *,
am Mittwoch, 5. November 2014 treffen wir uns um 19.00 in India King
für unser Hackathon. Bringt eure Laptops!
Themen:
- Agda: wir schreiben ein einfaches Hello World
oder
- Buch: Homotopy Type Theory (HoTT)
-- BERICHT --
26. Oktober 2014
- wir haben uns Categories for the working mathematician von Saunders
Mac Lane angeschaut.
- Das buch kann hier gefunden werden:
www.maths.ed.ac.uk/~aar/papers/maclanecat.pdf die Datei kann man aber
nicht durchsuchen weil es nur scans sind
- dieses Buch ist eine grundlegende Arbeit in Kategorientheorie
- das Text selbst ist sehr eigenständig; die Übungen machen aber
annahmen über sehr viel Wissen in abstrakte Algebra
- wir haben uns auch Category Theory von Steve Awodey angeschaut
- das buch ist viel langsamer als Mac Lane. Man kommt nur nach
mehreren Kapiteln zu interessanten Sachen
- die Übungen basieren nur auf Wissen aus den Buch
- das Buch ist einigermaßen kürzer als Mac Lane
- wir haben uns auch Homotopy Type Theory (HoTT) angeschaut. Es kann
hier gefunden werden: http://homotopytypetheory.org/book/
- thematisch ist das Buch zu den früheren beiden einigermaßen
unterschiedlich: hier geht es um Logik und Typsysteme die von grund
auf aufgebaut werden. Einige begriffe von Kategorientheorie werden
eingeführt.
- wobei Kategorientheorie das aller neuste vor 40 Jahren gewesen ist,
ist HoTT zur Zeit so zu sagen der Stand der Technik
- HoTT ist in sich komplett geschlossen. Es braucht nur sehr einfaches
Basiswissen aus Grundlagen der Mathematik
- Die Übungen basieren nur auf den Text und scheinen machbar zu sein
- Einige der späteren Übungen sind aber offene Forschungsprobleme
- Das buch ist so lange wie Mac Lane und Awodey zusammen
- Es wird von einer großen Gruppe von Experten geschrieben, unter
anderem Martin-Löf, Awodey, Aczel. Es wird ständig aktiv erweitert.
- Für HoTT kann man in Internet Code für Coq und Agda finden
- Es gibt auch aktive online Communities für HoTT
- wir werden in der Zukunft wahrscheinlich viel über HoTT und theorem
prover sprechen
-- ANFAHRT --
Wir treffen uns in India King, Landsbergerstr. 491.
Webseite: http://www.indiaking.de
Karte: https://goo.gl/maps/5g9m6
Anfahrtmöglichkeiten:
- S-Bahn nach Pasing nehmen (alle außer S1, S2 und S7) und dann Tram
19 nach Offenbachstraße (2 Haltestellen)
- Tram 19 von Hauptbahnhof richtung Pasing nehmen bis Offenbachstraße
- Bus 130 oder 131 zum Knie nehmen und dort in die Tram 19 nach Pasing
umsteigen, bis Offenbachstraße
- Bus 160 oder 162 nach Offenbachstraße
India King befindet sich genau gegenüber der Tramhaltestelle.
Twitter: https://twitter.com/Haskell_hackers
Web: http://haskell-hackathon.no-ip.org
English: http://haskell-hackathon.no-ip.org/index_en.html
Hi *,
am Sonntag, 2. November 2014 treffen wir uns um 18.00 in India King
für unser Hackathon. Bringt eure Laptops!
Die Hackathon-webseite ist jetzt auch auf Englisch! Das waren rund
100k text zu übersetzen... Viel spaß beim lesen!
http://haskell-hackathon.no-ip.org/index_en.html
Themen:
- proof systems: Isabelle/HOL, Agda, Coq
oder
- Buch: Homotopy Type Theory (HoTT)
-- BERICHT --
16. Oktober 2014
- ein Paar der Klasseninstanzen angeschaut: identitätsmonade,
funktoren und monoid für funktionen, ...
- mit Christine darüber gesprochen, wie man ein beginner-kurs für
Haskell betreiben könnte. Eine Idee war es, ein Buch in einer Gruppe
durchzulesen. Eine weitere Idee war es, Tutorials eins nach dem
anderen durchzugehen. Man könnte auch Übungen machen.
- darüber gesprochen, wie man eine Community betreiben soll; wie sie
sich entwickelt und wie man es schafft den zutritt neuer Teilnehmer
nicht zu verhindern.
- das Buch "Haskell-Intensivkurs" durchgeschaut:
http://www.amazon.de/Haskell-Intensivkurs-Kompakter-Funktionale-Programmier…
-- ANFAHRT --
Wir treffen uns in India King, Landsbergerstr. 491.
Webseite: http://www.indiaking.de
Karte: https://goo.gl/maps/5g9m6
Anfahrtmöglichkeiten:
- S-Bahn nach Pasing nehmen (alle außer S1, S2 und S7) und dann Tram
19 nach Offenbachstraße (2 Haltestellen)
- Tram 19 von Hauptbahnhof richtung Pasing nehmen bis Offenbachstraße
- Bus 130 oder 131 zum Knie nehmen und dort in die Tram 19 nach Pasing
umsteigen, bis Offenbachstraße
- Bus 160 oder 162 nach Offenbachstraße
India King befindet sich genau gegenüber der Tramhaltestelle.
Twitter: https://twitter.com/Haskell_hackers
Web: http://haskell-hackathon.no-ip.org