Haskell

[knivil]

Macht man in C++ doch auch.

Wie waere es, wenn du diese Aussage mit Argumenten untermauerst ...

[volkard]

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...

http://www.c-plusplus.net/forum/141881

[ertes]

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.

[CStoll]

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.

[ertes]

@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.

[Irgendwer]

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).

[CStoll]

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.

[wersglaubt]

DrGreenthumb schrieb:

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...

Du bist ja ganzschön dumm, wenn du meinst, dass man so die Korrektheit von Webseiten beweist.

knivil schrieb:

Beweist Haskell auch gleich numerische Stabilität und ähnliches? Sinnhaftigkeit von Spezifikationen?

Na, nu uebertreib mal nicht!

Damit wäre wohl alles dazu gesagt, was Haskell an Programmen beweisen kann, nämlich nichts was wirklich wichtig wäre.

[Irgendwer]

Das kannst du in C++ auch, wenn du verrückt genug bist - sowas nennt sich dann "Template Metaprogrammierung".

Es geht doch nicht darum, dass man das alles auch in C++ machen kann. Es geht darum, welche Sprache es einfacher macht die eigenen Vorstellungen umzusetzen. Dabei sind "Templates" in Haskell, die ein vollkommen natürlicher Bestandteil der Sprache sind (im Gegensatz zu Templates in C++), sehr angenehm zu benutzen. Selbst ein Anfänger kann quasi ohne Probleme die Definition von map aufschreiben. Schon aus dem Typ von map wird klar, wie es arbeitet:
map :: (a -> b) -> [a] -> [b]

Die "Schönheit", Ausdrucksstärke und Eleganz des Codes (die z.B. aus dem Typensystem resultiert) mag für manche nebensächlich sein, für mich ist sie allerdings einer der Hauptgründe für Haskell. Mag sein, dass Haskell nicht ganz so schnell ist wie C++, aber heutzutage ist es eben doch meistens schnell genug. Und für alles andere kann ich ja immer noch C++ verwenden, ist ja schließlich auch ein schönes Werkzeug.

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.

s.o.

Damit wäre wohl alles dazu gesagt, was Haskell an Programmen beweisen kann, nämlich nichts was wirklich wichtig wäre.

Doch, du kannst (im mathematischen Sinne) beweisen, dass dein numerisch stabiler Code auch korrekt ist.

[CStoll]

Irgendwer schrieb:

Das kannst du in C++ auch, wenn du verrückt genug bist - sowas nennt sich dann "Template Metaprogrammierung".

Es geht doch nicht darum, dass man das alles auch in C++ machen kann. Es geht darum, welche Sprache es einfacher macht die eigenen Vorstellungen umzusetzen. Dabei sind "Templates" in Haskell, die ein vollkommen natürlicher Bestandteil der Sprache sind (im Gegensatz zu Templates in C++), sehr angenehm zu benutzen. Selbst ein Anfänger kann quasi ohne Probleme die Definition von map aufschreiben. Schon aus dem Typ von map wird klar, wie es arbeitet:
map :: (a -> b) -> [a] ->

Das sagt mir aber auch nicht viel mehr als eine Funktions-Signatur in C++ - die Funktion nimmt eine unäre Funktion und eine Liste von Objekten und erzeugt daraus eine andere Liste von Objekten (OK, die sie gibt auch noch an, daß die beteiligten Typen zusammenpassen müssen). Um zu wissen, [b]was diese Funktion tatsächlich macht, mußt du dir doch ihre Definition ansehen. Genauso wie du aus dieser Signatur ihre Arbeitsweise ableiten kannst, kann ich das auch hieraus:

template< class InputIterator, class OutputIterator, class UnaryOperation >
OutputIterator transform( InputIterator first1, InputIterator last1,
                          OutputIterator d_first, UnaryOperation unary_op );

Nur für's Protokoll: Ich bin nicht unbedingt ein C++ Fanatiker, auch wenn ich hauptsächlich mit imperativen und objektorientierten Sprachen zu tun habe. Aber einige von euch scheinen die Mächtigkeit "eurer" Sprache zu überschätzen. (beide Sprachen sind afaik turing-vollständig, haben aber unterschiedliche Schwerpunkte - und beide Sprachen erfordern sicher einige Verrenkungen, um außerhalb ihrer Schwerpunktgebiete verwendet zu werden)

[wersglaubt]

Irgendwer schrieb:

Damit wäre wohl alles dazu gesagt, was Haskell an Programmen beweisen kann, nämlich nichts was wirklich wichtig wäre.

Doch, du kannst (im mathematischen Sinne) beweisen, dass dein numerisch stabiler Code auch korrekt ist.

Der zweite Teil ist der wichtige "Sinnhaftigkeit von Spezifikationen".

Ist doch ganz einfach. Man kann doch mit Haskell alles programmieren, also auch Fehler. Haskell weiß ganz sicher nicht, was ein Fehler im Programm ist, weil es keine Gedanken lesen kann, selbst wenn es das könnte, kann man damit nicht die Korrektheit von Webseiten oder ähnlichem beweisen, weil man nicht mal sicher sein kann, dass das was sich Menschen so denken, wie etwas funktionieren sollte, so korrekt ist.

[Irgendwer]

Aber einige von euch scheinen die Mächtigkeit "eurer" Sprache zu überschätzen.

Wenn man ertes Glauben schenkt, hat er auch schon mit imperativen Sprachen gearbeitet, sollte also in der Lage sein beide zu beurteilen. Wenn du ihm nicht glaubst (und auch den anderen nicht, die ähnliches behaupten), dann musst du wohl oder übel selbst ran und Haskell genausogut lernen wie C++ - dann kannst du selbst eine Aussage treffen.

(beide Sprachen sind afaik turing-vollständig, haben aber unterschiedliche Schwerpunkte - und beide Sprachen erfordern sicher einige Verrenkungen, um außerhalb ihrer Schwerpunktgebiete verwendet zu werden)

Sowohl Haskell als auch C++ haben keine Schwerpunktgebiete. Man verrenkt sich nur, wenn man versucht C++ in Haskell zu programmieren oder umgekehrt. Aber du gehst ja auch nicht ins Ausland und sprichst dort mit allen Deutsch, weil du es kannst und sie es gefälligst auch können sollen.

Genauso wie du aus dieser Signatur ihre Arbeitsweise ableiten kannst, kann ich das auch hieraus:

Jetzt bist du nur auf den letzten Satz meines Zitats eingegangen. Du musst zugeben, dass die Deklaration in C++ deutlich mehr "noise" beinhaltet als die Haskell-Version. Wie gesagt: Viele stört das nicht, aber ich schätze die Eleganz von Haskell sehr.

Um zu wissen, was diese Funktion tatsächlich macht, mußt du dir doch ihre Definition ansehen.

Ja, natürlich. Trotzdem schränkt diese Funktionsdefinition die Menge der Funktionen deutlich ein. IO kann z.B. nicht stattfinden.

Der zweite Teil ist der wichtige "Sinnhaftigkeit von Spezifikationen".

Darauf bin ich nicht eingegangen, weil der Gedanke allein schon total abstrus ist. Natürlich kann Haskell nicht zaubern - was erwartest du?

[CStoll]

Irgendwer schrieb:

Aber einige von euch scheinen die Mächtigkeit "eurer" Sprache zu überschätzen.

Wenn man ertes Glauben schenkt, hat er auch schon mit imperativen Sprachen gearbeitet, sollte also in der Lage sein beide zu beurteilen. Wenn du ihm nicht glaubst (und auch den anderen nicht, die ähnliches behaupten), dann musst du wohl oder übel selbst ran und Haskell genausogut lernen wie C++ - dann kannst du selbst eine Aussage treffen.

Entschuldige, wenn ich dafür nicht wirklich die Zeit habe, aber ich muß mich beruflich auf die Sprache konzentieren, die bei uns in der Firma verwendet wird. Und ich bezweifle, daß ich auf lange Sicht Gelegenheit bekomme, Haskell im Praxiseinsatz zu erleben.

(beide Sprachen sind afaik turing-vollständig, haben aber unterschiedliche Schwerpunkte - und beide Sprachen erfordern sicher einige Verrenkungen, um außerhalb ihrer Schwerpunktgebiete verwendet zu werden)

Sowohl Haskell als auch C++ haben keine Schwerpunktgebiete. Man verrenkt sich nur, wenn man versucht C++ in Haskell zu programmieren oder umgekehrt. Aber du gehst ja auch nicht ins Ausland und sprichst dort mit allen Deutsch, weil du es kannst und sie es gefälligst auch können sollen.

Ich nicht, aber um bei deiner Analogie zu bleiben, macht ihr hier genau das Ihr kommt als Haskell-Programmierer ins C++ Land und erwartet, daß hier jeder eure Sprache versteht.

Genauso wie du aus dieser Signatur ihre Arbeitsweise ableiten kannst, kann ich das auch hieraus:

Jetzt bist du nur auf den letzten Satz meines Zitats eingegangen. Du musst zugeben, dass die Deklaration in C++ deutlich mehr "noise" beinhaltet als die Haskell-Version. Wie gesagt: Viele stört das nicht, aber ich schätze die Eleganz von Haskell sehr.

Ich hätte auch die Template-Parameter mit I, O und F abkürzen können, aber ich mag es, wenn ein Bezeichner auch aussagt, was er darstellen will.
(btw, std::transform ist die Entsprechung zu map aus der C++ Standardbibliothek)

Um zu wissen, was diese Funktion tatsächlich macht, mußt du dir doch ihre Definition ansehen.

Ja, natürlich. Trotzdem schränkt diese Funktionsdefinition die Menge der Funktionen deutlich ein. IO kann z.B. nicht stattfinden.

Da die Funktion b-Objekte zurückliefern soll, wird sie diese irgendwie erzeugen - vermutlich mit der übergebenen (a->b) Funktion. Aber nach welcher Vorschrift der Rückgabewert zusammengesetzt wird, geht aus der Typdeklaration nicht hervor. Nimmt sie das erste Element der a-Liste und erzeugt eine Liste mit 100 Kopien von f(a0)? Füllt sie eine Liste mit zufällig permutierten f(an)-Werten? Liefert sie eine leere b-Liste? ...? Selbst ohne IO hast du da noch genug Freiheiten.

Der Compiler kann dir bestenfalls helfen, das Zusammenprallen von inkompatiblen Typen zu vermeiden. Er kann nicht sicherzustellen, daß du die einzelnen Werte korrekt miteinander verknüpfst.
Und selbst wenn du ihm sagst, was für ein Ergebnis bei einer Berechnung herauskommen soll - die Frage der Programm-Äquivalenz ist generell nicht entscheidbar. Und die meisten interessanten Programme dürften in den Bereich fallen, wo das relevant wird. (abgesehen davon, daß du einem Programm-Beweiser auch irgendwie mitteilen mußt, welches Funktion dein Programm berechnen soll)

[Irgendwer]

Entschuldige, wenn ich dafür nicht wirklich die Zeit habe, aber ich muß mich beruflich auf die Sprache konzentieren, die bei uns in der Firma verwendet wird.

Dafür brauchst du dich bei mir sicherlich nicht zu entschuldigen.

Ihr kommt als Haskell-Programmierer ins C++ Land und erwartet, daß hier jeder eure Sprache versteht.

Nö, gar nicht. Ich erwarte nur, dass man es nicht als "unnötig" und "unkomfortabel" abtut, bevor man sich nicht wirklich damit beschäftigt hat (siehe Startpost). Ich komme übrigens selbst von C++ und verwende es auch noch gerne (weiß also das funktionale std::transform zu schätzen ).

Ich hätte auch die Template-Parameter mit I, O und F abkürzen können, aber ich mag es, wenn ein Bezeichner auch aussagt, was er darstellen will.

Ich meinte eher die ganzen Schlüsselwörter, die spitzen Klammern und die Semikolons. Auch in Haskell macht es häufig Sinn sprechende Bezeichner zu wählen, auch wenn xs für eine Liste von x sehr geläufig ist.

Selbst ohne IO hast du da noch genug Freiheiten.

Ja, natürlich. Aber es kommt ja noch der Name der Funktion dazu, sowie die Annahme, dass der Autor sich bei dem Namen etwas gedacht hat. Ich will hier aber gar nicht so sehr drauf herumreiten, weil das alles - bis auf die Sache mit dem IO (die ich allerdings sehr wichtig finde) - auch für C++ und viele andere Sprachen gilt.

[CStoll]

Irgendwer schrieb:

Entschuldige, wenn ich dafür nicht wirklich die Zeit habe, aber ich muß mich beruflich auf die Sprache konzentieren, die bei uns in der Firma verwendet wird.

Dafür brauchst du dich bei mir sicherlich nicht zu entschuldigen.

Ihr kommt als Haskell-Programmierer ins C++ Land und erwartet, daß hier jeder eure Sprache versteht.

Nö, gar nicht. Ich erwarte nur, dass man es nicht als "unnötig" und "unkomfortabel" abtut, bevor man sich nicht wirklich damit beschäftigt hat (siehe Startpost).

Ich tue es auf jeden Fall nicht als unnötig ab, ich versuche nur, hier einigen Leuten klarzumachen, daß Haskell keine Wunderwaffe gegen alle Probleme der (Programmierer)Welt ist, als die es hier dargestellt wird. Solche Aussagen ala "Wenn es compiliert, ist es fehlerfrei" können vielleicht auf trivialeeinfache Programme zutreffen, aber bei größeren Projekten kommst du um echte Tests und Debugging auch nicht herum.

Ich hätte auch die Template-Parameter mit I, O und F abkürzen können, aber ich mag es, wenn ein Bezeichner auch aussagt, was er darstellen will.

Ich meinte eher die ganzen Schlüsselwörter, die spitzen Klammern und die Semikolons. Auch in Haskell macht es häufig Sinn sprechende Bezeichner zu wählen, auch wenn xs für eine Liste von x sehr geläufig ist.

Ich sehe es eher als Vorteil an, wenn sich die Sprachkonstrukte deutlich sichtbar erkennen lassen, auch wenn der Quelltext dadurch ein wenig länger wird.

Selbst ohne IO hast du da noch genug Freiheiten.

Ja, natürlich. Aber es kommt ja noch der Name der Funktion dazu, sowie die Annahme, dass der Autor sich bei dem Namen etwas gedacht hat. Ich will hier aber gar nicht so sehr drauf herumreiten, weil das alles - bis auf die Sache mit dem IO (die ich allerdings sehr wichtig finde) - auch für C++ und viele andere Sprachen gilt.

Da sind wir uns ja wenigstens in einem Punkt einig.
(übrigens sind Namen nur Schall und Rauch - und was jemand unter "map" versteht, hängt auch von seinen Vorkenntnissen ab)

[wersglaubt]

Irgendwer schrieb:

Der zweite Teil ist der wichtige "Sinnhaftigkeit von Spezifikationen".

Darauf bin ich nicht eingegangen, weil der Gedanke allein schon total abstrus ist. Natürlich kann Haskell nicht zaubern - was erwartest du?

Dass ihr nicht so tut, also ob Haskell zaubern kann.

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).

[!rr!rr_.]

kann jemand gerade mal in eins, zwei Sätzen Monaden und IO in Haskell erklären?

(und ich meine "Sätzen", nicht "Büchern")

[knivil]

@volkard: Wir haben ein anderes Verstaendnis von aequivalenten Umformungen bei Programmen. Deine ist auf Erfahrung begruendet, ich spreche aber von Gleichungen. Auch sind die Beipiele fuer Schleifen aus meiner Sicht recht duerftig. Und das Auslagern von Code in Funktionen dient hauptsaechlich einer besseren Programmstruktur. Mir ist klar, dass das selbst in C oder C++ nicht alles ist, aber ich meine etwas anderes.

Ueber Monads:
http://homepages.inf.ed.ac.uk/wadler/papers/marktoberdorf/baastad.pdf
http://www.haskell.org/tutorial/monads.html
http://www.haskell.org/haskellwiki/Monad

PS: Monads haben nicht primaer was mit IO zu tun.

gegen alle Probleme der (Programmierer)Welt ist

Bitte nenne die Probleme und ich kann dir sagen, wie Haskell im Vergleich zu imperativen Sprachen hilft.

größeren Projekten kommst du um echte Tests und Debugging auch nicht herum.

Hmm, meist werden groessere Projekte in imperativen Sprachen zu kleineren Projekten in funktionalen. Auch sind die aktuellen Debugging-Tools stark auf imperative Sprachen ausgelegt, so dass bei funktionalen nur Nachdenken hilft.

[ertes]

@CStoll: Ich will sehen, wie du in C++ einen Typen angibst, aus der sich nur die Identitätsfunktion ableiten lässt. In Haskell lässt sich aus der Spezifikation a → a genau eine mögliche Funktion ableiten, nämlich die Identitätsfunktion. Wenn du dein komplettes Programm in solchen Spezifikationen ausdrückst, kannst du auch dein Programm vollständig (automatisiert!) von den Typen ableiten. Dazu gibt es auch eine proof of concept-Implementierung, die sich djinn nennt.

Aber ich betone nochmal: So zu programmieren ist unpraktikabel, da man dafür fast im puren Lambda-Kalkül programmieren müsste, was sehr anstrengend ist. Das sehe ich also nicht als nennenswertes Feature für praxisorientierte Programmierung an. Es ist lediglich ein anschauliches Beispiel, wie weit man die Spezifizierung von Programmen treiben kann.

Dein Beispiel template metaprogramming hingegen erlaubt es nicht, Programme von Spezifikationen abzuleiten. Es erlaubt lediglich turingvollständige Programmierung im Template-System, also zur Kompilierzeit. Wenn du Programme, die Programme generieren, als Spezifikation siehst, hast du wahrscheinlich Recht, aber dann kann man in jeder Sprache Programme aus Spezifikationen ableiten. Ich sehe das anders.

Und was deine Kritik zu meiner Spezifikation angeht: Es war auch ein dämliches Beispiel. Wenn du das Ergebnis, das du suchst, so exakt wie möglich spezifizierst, dann schließt du viele Fehler aus. Beispiel: Du willst per IPv6 zum MX-Server einer Domain verbinden. Hier die wenig spezifizierte Variante:

resolveMx :: String → IO [String]
resolveAaaa :: String → IO String
connectTo :: String → Int → IO Handle
smtpSession :: Handle → IO ()

Hier die gut spezifizierte Variante und interessanterweise sogar flexiblere Variante:

resolveMx :: (Alternative f, DnsMonad m) ⇒ Domain → m (f Domain)
resolveAaaa :: (Alternative f, DnsMonad m) ⇒ Domain → m (f IPv6)
withConnection :: (IPAddress a, MonadPeelIO m) ⇒ a → PortID → (Handle → m b) → m b
smtpSession :: MonadIO m ⇒ Handle → m ()

Und jetzt eine Variante, bei der man kaum versehentlich einen Bug produzieren kann, der auch kompilierbar ist. Diese verhindert sogar, dass eine SMTP-Sitzung kompiliert, in der MAIL FROM vor EHLO gesendet wird (Resolver-Funktionen wie oben):

withConnection :: (IPAddress a, MonadPeelIO m) ⇒ a → PortID → (∀s. Handle s → Region s m b) → m b
smtpSession :: (MonadIO m, SmtpFullSession s) ⇒ MailT s m ()
runSmtpSession :: (MonadIO m, SmtpFullSession s) ⇒ MailT s m a → m a

ehlo :: SmtpFullSession so ⇒ Domain → (∀si. SmtpGreeted si ⇒ MailT si m b) → MailT so m b
mailFrom :: SmtpGreeted so ⇒ String → (∀si. SmtpHaveFrom si ⇒ MailT si m b) → MailT so m ()
rcptTo :: SmtpHaveFrom so ⇒ [String] → (∀si. SmtpHaveTo si ⇒ MailT si m b) → MailT so m ()

Jetzt bin ich aber tatsächlich so weit, dass ich ein Beispiel poste, mit dem wahrscheinlich außer Haskell-Programmierern keiner was anfangen kann. Aber es zeigt, wie weit man den Korrektheitskram treiben kann, und zwar in einem sehr praktischen Beispiel: eine SMTP-Implementierung. Man kann die Spezifikation so einengen, dass fatale Exceptions (RAM verbraucht, SIGILL, etc.) die einzige Möglichkeit sind für ein Programm, um von der Spezifikation abzuweichen. Und dann kannst du noch so weit gehen, diese an geeigneten Stellen abzufangen und spezifikationsbasiert zu verarbeiten. Wie genau du spezifizierst, ist dir überlassen.

Ich persönlich begnüge mich mit etwas einfacheren Spezifikationen, also die zweite Variante. Das reicht mir. Sie garantieren mir nicht, dass meine SMTP-Sitzungen konform sind, aber sie garantieren, dass in meinem Programm nirgendwo ein ungültiges Socket-Handle existieren kann und dass mein Programm keinen String von einem Socket verarbeitet, der nicht vorher durch einen Längenfilter gejagt wurde, um DoS-Angriffe mit unendlichen Strings o.ä. abzuwehren.

Und bevor wieder irgendjemand seinen Senf abgibt, der keine Ahnung von Haskell hat: Die Sonderzeichen im Code (∀, →, ⇒) schreibt man normalerweise als ASCII-Annäherungen im Code (forall, ->, =>). Da aber auch die Unicode-Zeichen erlaubt sind, verwende ich hier die lesbareren echten Symbole.

Aber jetzt zum dritten mal: Das ist ein nettes Feature, aber nicht mein Hauptgrund für Haskell. Mein Hauptgrund ist das gute Concurrency-System, die vielen brauchbaren Design-Patterns, die sehr nette Community, etc. Warum sind Haskell-Programme wohl so kurz? Weil man sie zu Tode spezifizieren kann? Ganz bestimmt nicht. Das spart einem nur sehr viel Debugging-Zeit. Also vergesst einfach das mit der Korrektheit wieder, denn das ist in einem C++-Forum so wie so nicht objektiv zu diskutieren. Nur wer Haskell gut kennt, kann das auch wirklich gut beurteilen, und hier scheint keiner dabei zu sein, der das von sich behaupten kann.

Und zum zweiten mal: Ich teste meine Programme sehr genau. Dass ich kaum Debugging-Zeit habe, heißt nicht, dass ich nicht teste. Es heißt nicht, dass ich mich blind auf meine Spezifikation verlasse. Es heißt lediglich, dass ich meine Spezifikation gut genug schreibe, um eine sehr weite Klasse von Bugs schon zur Kompilierzeit auszuschließen, sodass mein Programm in der Testphase sich meistens genau so verhält wie es soll. Ich kann ernsthaft nicht sagen, wann ich zum letzten mal wirklich debuggt habe (unwirkliches Debugging = einen Rechtschreibfehler in einem UI-String korrigieren). Und jeder, der erzählt, dass sowas unmöglich/nur Spielerei/blödsinnig ist, unterstellt mir in einem direkten persönlichen Angriff, dass ich die letzten paar Jahre nur geträumt habe, dass ich als Programmierer völlig unfähig bin, dass ich lüge oder dass ich nur "triviale" oder "einfache" Programme schreibe, was alles falsch ist.

Und schließlich zum Abschluss: Hier geben viele Leute sehr unqualifizierten Müll über Haskell ab, obwohl sie die Sprache überhaupt nicht verstehen. Und nein, es reicht nicht, sie sich mal kurz angesehen zu haben. Haskell hat eine steile Lernkurve (einer ihrer Nachteile) und selbst die alten Hasen erklimmen sie noch, denn in dieser Sprache lernt man nie aus. In Haskell ist vieles möglich, was der durchschnittliche C++-Programmierer für unmöglich hält oder sich in seiner C++-Denkweise gar nicht vorstellen kann. Aber das ist eben das Blub-Paradoxon. Hier spielt C++ die Rolle von Blub. Kernaussage des Artikels: Der gläubige C++-Programmierer wird nie akzeptieren können, dass es eine Sprache gibt, die C++ übertrifft. Ich will nicht sagen, dass ich kein gläubiger Haskell-Programmierer bin, aber ich war früher genau wie ihr: ein gläubiger C++-Programmierer. Ich habe gelernt, dass es von Nachteil ist, sich auf seine Ansichten zu versteifen. Daher probiere ich immer wieder neue Dinge aus, darunter auch Technologien, die noch nicht weit verbreitet, sehr anders und experimentell sind. Haskell ist eine davon.

Wenn mir jetzt jemand mit einer Sprache kommt, die mächtiger ist als Haskell – und die gibt es definitiv, siehe z.B. Agda oder Coq – dann würde ich heute nicht mehr widersprechen. Agda etwa ist in vielerlei Hinsicht wesentlich mächtiger als Haskell, aber leider existieren kaum praxisrelevante Bibliotheken dafür. Bisher gibt es nur ein paar proofs of concept wie etwa Lemmachine, ein HTTP-Framework, dessen Korrektheit vollständig statisch bewiesen wird. Das, wofür man in Haskell (wie oben erwähnt) fast im reinen Lambda-Kalkül programmieren müsste, lässt sich in Agda in sehr praktikablem Code machen. Tatsächlich ist Agda sogar nicht turingvollständig, denn um die vollständige Beweisbarkeit etwa von einem Webserver praktikabel zu machen, darf man schon mal keine Endlosschleifen erlauben.

Und bevor jetzt jemand kommt, der keine Ahnung von Agda hat: Man kann trotzdem jedes beliebige Programm ausdrücken. Ja, auch ein Programm, das endlos läuft. Siehe Kodaten und Korekursion. Und ich bin mir sicher, dass nach meiner Aussage über die Turingvollständigkeit von Agda den meisten hier die Finger gebrannt haben zu behaupten, wie bescheuert denn Agda sein muss, und wie dumm jemand sein muss, der in Agda programmiert, etc. pp., ohne sich auch nur ein einziges mal die Mühe gemacht zu haben, sich die Sprache erst mal anzusehen.

So, das war nun ein ziemlich langer Post. Ich hoffe, es macht sich der eine oder andere die Mühe, ihn richtig zu lesen und zu verstehen, bevor er auf den Antwort-Link klickt.

[volkard]

ertes schrieb:

...

Wenn ich in C++ nur die Prototypen der Kontruktoren recht definiere, kann ich exakt das gleiche erzeugen. Aber es ist ebenso ein Quatsch, weil zu mühsam zu programmieren. Eine relativ nutzlose Spielerei, die ich schon vor 20 Jahren zum Exzess gebracht hatte und weitgehend verworfen. In C++ benutze ich was, was in der Nähe der "gut spezifizierten Variante" ist. Bei Sockets, Servern und Clients. Aber nicht bei Primzahlen.