Haskell
-
Irgendwer schrieb:
Sag doch mal klar und deutlich was du meinst, anstatt dir irgendwelche Einzelaussagen herauszugreifen und diese zu kritisieren. Das würde eine Diskussion deutlich einfacher machen...
Ein anderes Vokabular übrigens auch.
knivil schrieb:
Bullshit! [...]
@volkard: Bullshit! [...]Warum nicht auch mal Schafkot oder Ziegenmist? Oder Argumente stattdessen?
-
knivil schrieb:
Bullshit, Haskell hat besseres OOP!
... besser als wer?
Und mal her mit einem Beispiel, an dem man das erkennen kann!
-
@Irgendwer:
Nun, ich nehme dieses Thema sehr locker, da ich etwa die gleiche Ansicht vertrete wie Paul Graham, aber nicht auf Common Lisp bezogen, sondern auf Haskell. Mir kommt es zugute, dass meine Konkurrenz Haskell nicht kennt oder davon nicht viel hält. Das bringt mir bares Geld, und keiner scheint zu verstehen, wie ich das mache. Das ist gut für mich. In diesem Sinne schneide ich mir eigentlich ins eigene Fleisch, indem ich hier poste, aber ich bin eben nicht so konsequent wie Paul.Fakt ist: Haskell hat meine Entwicklungszyklen dramatisch verkürzt. Ich mache praktisch kein Debugging mehr, denn sobald meine Programme kompilieren, funktionieren sie auch. Nein, ich meine nicht nur, dass ihre Korrektheit bewiesen ist, sondern dass sie sich auch in der Praxis beweist. Und dabei geht es nicht um irgendwelchen akademischen Kram, sondern um praktische Anwendungen, mit denen ich Geld verdiene (Webseiten hauptsächlich).
Es kommt nicht selten vor, dass ich seitenweise Code schreibe, bevor ich auch nur ein einziges mal kompiliere. Meistens habe ich dann ein bis zwei Typfehler drin (die in C++ zu 99% zu Laufzeitfehlern führen würden). Die behebe ich, und schon funktioniert mein Code. Da können die ganzen C++-Freaks hier noch so wenig von automatischen Beweisverfahren durch Typentheorie halten. Es ist Fakt. Und dadurch kann ich mich auf die eigentliche Aufgabe konzentrieren und Code schreiben, der etwas tut. Das ist vielleicht auch der Grund dafür, dass es keinen anspruchsvollen Debugger für Haskell gibt. Er wird schlicht und ergreifend nicht gebraucht. Und nochmal: Klar werden jetzt jedem C++-Programmierer die Finger jucken, mir zu widersprechen, aber das interessiert mich nicht. Es ist Fakt, und mit diesem Fakt verdiene ich Geld.
Mir wird so oft widersprochen, wenn ich sage, dass Haskell eine geniale Sprache ist. Inzwischen spare ich mir diese Aussage, denn ich kenne die Macht von Haskell und weiß sie zu schätzen, und ich gehöre zu denen, die den direkten Vergleich haben und demnach objektiv beurteilen können. Und wenn man mir nicht glaubt, ist das besser für mich.
-
ertes schrieb:
Klar werden jetzt jedem C++-Programmierer die Finger jucken, mir zu widersprechen
nicht jedem! manch einer beneidet dich und würde viel lieber auch haskell programmieren...
-
ertes schrieb:
Fakt ist: Haskell hat meine Entwicklungszyklen dramatisch verkürzt. Ich mache praktisch kein Debugging mehr, denn sobald meine Programme kompilieren, funktionieren sie auch. Nein, ich meine nicht nur, dass ihre Korrektheit bewiesen ist, sondern dass sie sich auch in der Praxis beweist. Und dabei geht es nicht um irgendwelchen akademischen Kram, sondern um praktische Anwendungen, mit denen ich Geld verdiene (Webseiten hauptsächlich).
Müssen aber total simple Seiten sein. Wie kann man überhaupt die Korrektheit von Webseiten beweisen?
Bei den meisten Anwendungen ist das Problem doch, dass die Kunden etwas wollen und wenn man das macht, merken sie, dass sie was anderes brauchen.
-
wersglaubt schrieb:
Müssen aber total simple Seiten sein. Wie kann man überhaupt die Korrektheit von Webseiten beweisen?
hinter den Webseiten die Du als Benutzer siehst, arbeiten Programme...
Bei den meisten Anwendungen ist das Problem doch, dass die Kunden etwas wollen und wenn man das macht, merken sie, dass sie was anderes brauchen.
darum lieber schnell Ergebnisse schaffen.
-
@ertes: Auch auf die Gefahr hin, bereits genannte Argumente zu wiederholen:
Es ist mathematisch (?) nicht möglich, die Korrektheit eines Programms zu beweisen - außer du schränkst die Sprache so weit ein, daß du nicht mehr jedes Problem damit lösen kannst. Damit haben sich schon Generationen von Informatikern beschäftigt (Stichwort: Berechenbarkeit).
Und selbst wenn der Compiler dein Programm akzeptiert, wer sagt dir, daß es wirklich die Aufgabe löst, die du gestellt bekommen hast? Vielleicht hattest du ja auf deinen "seitenweise Code" einen Denkfehler, der das komplette Ergebnis verfälscht.
-
ertes schrieb:
Es kommt nicht selten vor, dass ich seitenweise Code schreibe, bevor ich auch nur ein einziges mal kompiliere. Meistens habe ich dann ein bis zwei Typfehler drin (die in C++ zu 99% zu Laufzeitfehlern führen würden). Die behebe ich, und schon funktioniert mein Code.
Und was wenn man mal etwas komplexere Aufgaben hat? Beweist Haskell auch gleich numerische Stabilität und ähnliches? Sinnhaftigkeit von Spezifikationen? Wie sichert man ab, dass der Code im realen Umfeld überhaupt läuft (hinsichtlich Resourcen)? Dieses ganze blabla von wegen kompiliert also läufts ist einfach nur oberflächlicher Bullshit.
Edit: Und nein, ich habe nichts gegen Haskell, würde ich mir gerne mal anschauen wenn ich Zeit dazu hätte.
-
ertes schrieb:
Huch, warum denn an mich gerichtet? Ich sehe das eigentlich so ähnlich wie du.
Tim schrieb:
Dieses ganze blabla von wegen kompiliert also läufts ist einfach nur oberflächlicher Bullshit.
Er spricht doch nur von seiner Erfahrung, wobei ich schon von vielen anderen Haskellern ähnliches gehört habe. Sind aber wahrscheinlich alles Lüger.
CStoll schrieb:
Vielleicht hattest du ja auf deinen "seitenweise Code" einen Denkfehler, der das komplette Ergebnis verfälscht.
Es sagt doch niemand, dass man nicht testen darf. Ich bin sicher selbst ertes wird kein Programm an einen Kunden ausliefern, dass er nicht vorher getestet hat.
-
Es ist mathematisch (?) nicht möglich, die Korrektheit eines Programms zu beweisen
Falsch! Die richtige Aussage lautet: Es ist allgemein nicht moeglich ... . D.h. fuer ausgewaehlte Programme ist durchaus moeglich. Es hat nichts mit der Sprache sondern nur was mit dem Anwendungsfall zu tun. Und es gibt recht viele Anwendungsfaelle, wo das moeglich ist. Meist geht es auch nicht um ein gesamtes Programm angefangen bei Userinput bis hin zum Drucken von Dokumenten.
Und was wenn man mal etwas komplexere Aufgaben hat?
Was sind komplexe Aufgaben?
Beweist Haskell auch gleich numerische Stabilität und ähnliches? Sinnhaftigkeit von Spezifikationen?
Na, nu uebertreib mal nicht!
Wie sichert man ab, dass der Code im realen Umfeld überhaupt läuft (hinsichtlich Resourcen)?
Die statische Analyse von ghc ist recht gut.
Dieses ganze blabla von wegen kompiliert also läufts ist einfach nur oberflächlicher Bullshit.
Nur solange man nicht unter die Haube von ghc geschaut hat. Was man dort sieht, kann man nicht Forum-gerecht wiedergeben. Jeder muss sich selbst ueberzeugen.
-
knivil schrieb:
Es ist mathematisch (?) nicht möglich, die Korrektheit eines Programms zu beweisen
Falsch! Die richtige Aussage lautet: Es ist allgemein nicht moeglich ... . D.h. fuer ausgewaehlte Programme ist durchaus moeglich. Es hat nichts mit der Sprache sondern nur was mit dem Anwendungsfall zu tun. Und es gibt recht viele Anwendungsfaelle, wo das moeglich ist. Meist geht es auch nicht um ein gesamtes Programm angefangen bei Userinput bis hin zum Drucken von Dokumenten.
Du kannst beweisen, daß das Richtige gedruckt wird?
-
wenn die Spezifikation vom Kunden von vornherein unabänderlich feststeht, kann man fast in jeder Programmiersprache zügig und korrekt implementieren.
Wie hier schon gesagt wurde, trennt sich die Spreu vom Weizen, wenn der Kunde hinterher merkt, daß er eigentlich was anderes will, als er vorher gesagt hat.
Bezweifle mal, daß funktionale Sprachen in solchen Fällen ggü "klassischen" Sprachen im Vorteil sind. Tippe da eher auf dynamische OO-Sprachen.
-
wenn die Spezifikation vom Kunden von vornherein unabänderlich feststeht, kann man fast in jeder Programmiersprache zügig und korrekt implementieren.
Unabänderlich reicht nicht, sie muss auch vollständig und widerspruchsfrei sein. Das ist bei komplexen Aufgaben in der Regel nicht gegeben.
-
Du kannst beweisen, daß das Richtige gedruckt wird?
Ich versuchte auszudruecken, dass es gerade darum nicht geht.
wenn die Spezifikation vom Kunden von vornherein unabänderlich feststeht, kann man fast in jeder Programmiersprache zügig und korrekt implementieren.
Das bezweifelt niemand. Es ist aber ein Unterschied ob man Assembler, C++ oder gar Haskell verwendet.
Tippe da eher auf dynamische OO-Sprachen.
Raten hilft nicht, nur ausprobieren! Warum sollten OO-Sprachen besser geeignet sein als funktionale? Fuer einen Vergleich reicht es nicht, nur eine Seite zu kennen!
-
knivil schrieb:
Und was wenn man mal etwas komplexere Aufgaben hat?
Was sind komplexe Aufgaben?
Ich sag mal: Das Generieren von Webseiten als Ein-Mann-Projekt zählt nicht dazu.
knivil schrieb:
Beweist Haskell auch gleich numerische Stabilität und ähnliches? Sinnhaftigkeit von Spezifikationen?
Na, nu uebertreib mal nicht!
Da ich nicht derjenige hier bin der sagt "kompiliert also geht" bin ich wohl kaum der Übertreibende. Aber so langsam bekomme ich den Eindruck, dass ihr euch dieses "geht" einfach anders hindefiniert.
knivil schrieb:
Dieses ganze blabla von wegen kompiliert also läufts ist einfach nur oberflächlicher Bullshit.
Nur solange man nicht unter die Haube von ghc geschaut hat. Was man dort sieht, kann man nicht Forum-gerecht wiedergeben. Jeder muss sich selbst ueberzeugen.
Dann überzeuge mich. Was passiert wenn ich z.B. die Klammerung in einer Berechnung falsch setze? Das Programm wird idR kompilieren, aber das Ergebnis wird nicht das sein das ich will. Wie geht man dieses Problem in Haskell an? Testen tut man ja offensichtlich nicht, also wie beweist man sowas?
-
@Tim:
Wie geht man dieses Problem in Haskell an?
Die Programmiersprache kann nur im Rahmen der Programmiersprache unterstuetzend wirken, also auf Basis von Typen, Rekursion und Funktionen. Sie wird schwer ein + anmahnen, wenn ein - gemeint ist. + und - besitzen den gleichen Typ. Sowas wuerde ich persoenlich als Schusselfehler einstufen.
Beweisen ... kann man natuerlich nur Behauptungen. Behauptungen in der Mathematik sind Aussagen der Form A = B, wobei vielleicht A eine Funktion f(x) ist und B das Programm. Testen ist ein Spezialfall: 55 = B(1,2,3). Wenn ich aber zeigen kann, dass f(x) = B(a,b,c) ist, dann brauche ich nicht zu testen. Ein sehr einfaches Beispiel ist:
filter p (xs ++ ys) = (filter p xs) ++ (filter p ys)
Ich kann also die gesamte Liste (xs ++ ys) am Stueck verarbeiten oder die Arbeit auf beiden Teillisten erst ausfuehren und das Ergenis danach zusammenfuehren. Ein guter Ansatz fuer Parallelisierung, wenn das Zerlegen in Teile billig im Vergleich zu p ist.
map f (map g xs) = map (f.g) xs
Ein Beispiel fuer Programmfusion (light). Ich brauche nur einmal ueber die Liste xs iterieren. Wie weit man damit kommt, laesst sich beispielsweise in Programming in Haskell Kapitel 11 nachlesen.
Andersherum kann man aus einem Programm durch aequivalente Umformung ein neues ableiten, dass womoeglich ein besseres Laufzeitverhalten hat. In Grundlagen funktionaler Programmierung von Martin Erwig wird fuer die maximale Teilsumme aus einem O(n^3) der Algorithmus mit O(n) durch aequivalente Umformungen angegeben. Der Kompiler selbst kann diese Umformungen nicht automatisch ausfuehren, er braucht zumindestens gelegentliche Hinweise oder Annotationen. ghc selbst enthaelt schon viel von diesem Expertenwissen und kann auf dieser Basis gut Optimieren. Weitere anlaufstelle: Bird-Meertens Formalism. Das sind nur die Grundlagen ... interessant wird es dann bei der korrekten Implementation von beispielsweise des Barnes-Hut-Algorithmuses, aber bitte parallel.
Dann überzeuge mich.
Nein! Ich kann dir nur zeigen, wo du selbst nachlesen kannst. Ueberzeugen musst du dich selbst.
-
knivil schrieb:
aequivalente Umformung
Macht man in C++ doch auch.
Anfänger und die "Webdesigner" um Dich tun es nicht, aber mit denen vergleichst Du Dich hoffentlich nicht.
-
Macht man in C++ doch auch.
Wie waere es, wenn du diese Aussage mit Argumenten untermauerst ...
-
knivil schrieb:
Macht man in C++ doch auch.
Wie waere es, wenn du diese Aussage mit Argumenten untermauerst ...
Die wichtigte Transformation ist sicherlich, innere Schleifen in Funktionen auszulagern. Aber auch Schleifen ein paar Zeilen unwinden oder winden, um das innere break an den Rand zu bekommen, arithmetische Umformungen, auch von Schleifenbedingungen, das Problem in zwei halbe zerlegen für divide&conquer, und ein ganzer Haufen von weiteren Mustern, die man einfach erkennt und umsetzt, ohne dabei noch über den Inhalt nachdenken zu müssen.
Wenn nach ein paar Umformungen übrigbleibt,if(bedingung) do tuwas() while(bedingung);dann fliegen die Finger von allein und machen draus
while(bedingung) tuwas()Bei mir weniger "aequivalente Umformung", sondern mein Name war "formale Transformation", wobei die Betonung auf "formal" liegt, die kann man durchziehen, ohne sich zu vergegenwärtigen, was sie bedeutet, man muß nicht nachdenken, ob sie zu korrektem Code führt. War der EIngangscode korrekt, ist der Ausgangscode auch korrekt.
Ich schreibe nicht den tollsten Code auf Anhieb, weil ich anfangs das Problem und was ich überhaupt will, noch gar nicht verstanden habe. Aber dann mache ich formale Transformationen, der Code vereinfacht sich Zug um Zug und bald kann ich ihn sogar verstehen. Dann ist er gut und kann so bleiben. Außer, ich sehe dann plötzlich sinnvolle (nicht formale) Transformationen, die mache ich halt auch und es schließen sich wieder ein paar formale an...
-
CStoll schrieb:
@ertes: Auch auf die Gefahr hin, bereits genannte Argumente zu wiederholen:
Es ist mathematisch (?) nicht möglich, die Korrektheit eines Programms zu beweisen - außer du schränkst die Sprache so weit ein, daß du nicht mehr jedes Problem damit lösen kannst. Damit haben sich schon Generationen von Informatikern beschäftigt (Stichwort: Berechenbarkeit).
Und selbst wenn der Compiler dein Programm akzeptiert, wer sagt dir, daß es wirklich die Aufgabe löst, die du gestellt bekommen hast? Vielleicht hattest du ja auf deinen "seitenweise Code" einen Denkfehler, der das komplette Ergebnis verfälscht.Wer sagt denn, dass ich meine Programme nicht teste? Sonst weiß ich ja nicht, ob sie funktionieren oder nicht. Ich verlasse mich ja nicht Blind auf mein Typensystem. Es ist nur so, dass es mich meistens vor meiner eigenen Menschlichkeit rettet.
Zur Beweisbarkeit von Programmen: Siehe Curry-Howard-Isomorphismus. In Haskell existiert eine starke Bindung zwischen dem Typensystem und der Aussagenlogik. Wenn du richtig Haskell programmierst, sind die Typen, die du zuweist, die Spezifikation deines Programms. Das ist genau der Grund, warum ich Typinferenz nur beschränkt verwende. Ich schreibe lieber explizite Typensignaturen, und zwar bevor ich die dazugehörigen Funktionen/Werte schreibe. Entspricht dein Programm nicht der Spezifikation, dann hast du auf jeden Fall einen Fehler im Code. Entspricht der Code deiner Spezifikation, dann funktioniert er auch. Wenn der Code trotzdem nicht das tut, was du willst, dann liegt der Fehler nicht im Code, sondern dann ist deine Spezifikation falsch oder nicht hinreichend.
Und das ist genau die Kunst von Haskell: Einerseits richtige, stichhaltige Spezifikationen schreiben, andererseits auch die ganzen Eigenschaften nutzen, die dich produktiver machen. Haskells Vorteile liegen ja nicht allein in der Korrektheit von Programmen. Du hast ein ziemlich geniales Laufzeitsystem und viele sehr effiziente Design Patterns, die du in anderen Sprachen nicht richtig ausdrücken kannst. Deswegen sagt dir auch jeder erfahrene Haskell-Programmierer: Haskell hat deshalb so schlechten OOP-Support, weil es eben einfach nicht gebraucht wird.
Tim schrieb:
Und was wenn man mal etwas komplexere Aufgaben hat? Beweist Haskell auch gleich numerische Stabilität und ähnliches?
Ja – sofern in deiner Spezifikation vorgesehen.
Sinnhaftigkeit von Spezifikationen?
Nein. Siehe oben. Wenn die Spezifikation Blödsinn ist, dann akzeptiert der Compiler natürlich auch nur Programme, die genau diesen Blödsinn veranstalten. Allerdings ist auch das ein Vorteil: Wenn du deiner Quadratwurzelfunktion den Typ Double → String zuweist, aber eine sinnvolle Funktion schreibst, wird der Compiler meckern. Die Funktion entspricht nicht deiner Spezifikation. Und beim Versuch, die Funktion der Spezifikation anzupassen merkst du, dass deine Spezifikation keinen Sinn ergibt.
Wie sichert man ab, dass der Code im realen Umfeld überhaupt läuft (hinsichtlich Resourcen)?
Indem man genug Resourcen zur Verfügung stellt? Was ist denn das für eine bescheuerte Frage?
Dieses ganze blabla von wegen kompiliert also läufts ist einfach nur oberflächlicher Bullshit.
Ein Programm kompiliert genau dann, wenn es der Spezifikation entspricht. Ist deine Spezifikation Quatsch, dann kann auch nur Quatsch dabei rauskommen. Nimm die Tatsache, dass du in C++ Variablen- und Funktionstypen angeben musst (int x, double sqrt(double)), und treibe sie an die Spitze. Dann hast du einen kleinen Eindruck von Haskell, aber nur einen kleinen, denn Haskells Typensystem erlaubt dir, exakt zu spezifizieren, was dein Programm tun soll. Das kann das Typensystem von C++ nicht.
volkard schrieb:
Du kannst beweisen, daß das Richtige gedruckt wird?
Du kannst beweisen, dass das Richtige zum Drucker gesendet wird.
Bashar schrieb:
wenn die Spezifikation vom Kunden von vornherein unabänderlich feststeht, kann man fast in jeder Programmiersprache zügig und korrekt implementieren.
Unabänderlich reicht nicht, sie muss auch vollständig und widerspruchsfrei sein. Das ist bei komplexen Aufgaben in der Regel nicht gegeben.
Und genau das kann Haskell dir bescheinigen. Ergibt die Spezifikation keinen Sinn, wird der Compiler ebenso meckern wie wenn die Spezifikation stimmt, aber das Programm nicht. Beispiel: In Haskell kannst du ausdrücken, dass ein Handle (entspricht etwa FILE bzw. iostream) nur innerhalb eines bestimmten Funktionsabschlusses verwendet werden darf. Dann ist es unmöglich, eine Funktion auszudrücken, die dieses Handle per IPC an einen anderen Thread übergibt. Die Spezifikation letzterer Funktion würde keinen Sinn ergeben und vom Compiler abgelehnt werden.
Tim schrieb:
Dann überzeuge mich. Was passiert wenn ich z.B. die Klammerung in einer Berechnung falsch setze? Das Programm wird idR kompilieren, aber das Ergebnis wird nicht das sein das ich will. Wie geht man dieses Problem in Haskell an? Testen tut man ja offensichtlich nicht, also wie beweist man sowas?
Wenn man wirklich so weit gehen will, geht auch das. Beispiel:
(.+.) :: Num a => a -> a -> Sum (.*.) :: Sum -> Sum -> Product -- Kompiliert: (3 .+. 3) .*. 4 -- Kompiliert nicht: 3 .+. 3 .*. 4 3 .+. (3 .*. 4)An alle: Ihr geht alle davon aus, dass ich Haskell so toll finde, weil es mir hilft korrekte Programme zu schreiben. Das ist natürlich einer der Gründe, aber bei Weitem nicht der wesentliche. Haskell erlaubt es mir, auf sehr einfache Art Webseiten oder skalierbare Serverprogramme zu schreiben. Genau dafür setze ich es ein. Es ist sehr leicht, korrekte konkurrente und/oder parallele Programme zu schreiben.