Haskell

[knivil]

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

[volkard]

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.

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