Haskell
-
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.
-
Ich gebe ja zu, daß ich mich mit Haskell nicht sonderlich auskenne, aber für mich hört sich das nicht sehr flexibel an.
(.+.) :: Num a => a -> a -> Sum (.*.) :: Sum -> Sum -> Product -- Kompiliert: (3 .+. 3) .*. 4 -- Kompiliert nicht: 3 .+. 3 .*. 4 3 .+. (3 .*. 4)Und was mache ich, wenn ich an einer anderen Stelle des Programms eine der letzteren Verianten benötige? Noch mehr Operatoren schreiben, für eine andere spezielle Kombination genutzt werden können?
PS: Und aus der Aussage, daß der Plus-Operator zwei beliebige Objekte nimmt und daraus eine Summe macht, lässt sich noch gar nichts über die Semantik dieser Operation aussagen.
-
@CStoll: Du kannst es so weit verfeinern, bis du dein Programm komplett von seinen Typen ableiten kannst. Deswegen habe ich mich auf den Curry-Howard-Isomorphismus bezogen. Aber das macht man in der Praxis nicht, zumindest ich nicht. Es gibt bestimmt Leute, die verrückt genug sind.
Mir reicht eine saubere, praktische Spezifikation aus. Das verhindert Bugs nicht, kann sie aber stark minimieren. Und nochmal: Korrektheitsprüfung ist für mich nicht der ausschlaggebende Punkt. Ich schreibe wenig Code, der viel tut und trotzdem noch (für einen Haskell-Programmierer) sehr gut lesbar ist.
-
Ich gebe ja zu, daß ich mich mit Haskell nicht sonderlich auskenne, aber für mich hört sich das nicht sehr flexibel an.
Wie soll es auch? Die Problemstellung "Haskell soll mir verbieten ein + statt einem * zu schreiben" ist ja auch dämlich. Das ist ganz klar ein Logikfehler, vor dem dich keine Sprache der Welt schützen kann.
PS: Und aus der Aussage, daß der Plus-Operator zwei beliebige Objekte nimmt und daraus eine Summe macht, lässt sich noch gar nichts über die Semantik dieser Operation aussagen.
Er nimmt nicht zwei beliebige Objekte. Er nimmt zwei Objekte des selben Typs, welcher zusätzlich noch das Num Interface implementieren muss. Wenn man dem Autor von .+. keine bösen Absichten unterstellt, ist allein wegen der Typen klar, wie die Funktion arbeitet. Natürlich könnte man etwas ähnliches auch in C++ erreichen, allerdings nur halb so schön (da keine eigenen Operatoren erlaubt sind).
-
ertes schrieb:
@CStoll: Du kannst es so weit verfeinern, bis du dein Programm komplett von seinen Typen ableiten kannst. Deswegen habe ich mich auf den Curry-Howard-Isomorphismus bezogen. Aber das macht man in der Praxis nicht, zumindest ich nicht. Es gibt bestimmt Leute, die verrückt genug sind.
Das kannst du in C++ auch, wenn du verrückt genug bist - sowas nennt sich dann "Template Metaprogrammierung".
Edit:
Irgendwer schrieb:
PS: Und aus der Aussage, daß der Plus-Operator zwei beliebige Objekte nimmt und daraus eine Summe macht, lässt sich noch gar nichts über die Semantik dieser Operation aussagen.
Er nimmt nicht zwei beliebige Objekte. Er nimmt zwei Objekte des selben Typs, welcher zusätzlich noch das Num Interface implementieren muss. Wenn man dem Autor von .+. keine bösen Absichten unterstellt, ist allein wegen der Typen klar, wie die Funktion arbeitet. Natürlich könnte man etwas ähnliches auch in C++ erreichen, allerdings nur halb so schön (da keine eigenen Operatoren erlaubt sind).
Klar muß man mit C++ mit den vorgegebenen Operator-Bezeichnungen auskommen, aber die kann man für eigene Klassen problemlos überladen. Und mit Templates kann man auch Funktionen für (beinahe) beliebige Typen aufbauen.