Haskell

[Zeus]

ertes schrieb:

Zeus schrieb:

Sieht aus wie Nischen-Frameworks aus, Schade

Natürlich sind die Frameworks nicht weit verbreitet, aber deswegen sind sie nicht ungeeignet. Wenn du Interesse hast, einfach mal ausprobieren. Ich wüsste nicht, was etwa in Yesod schwerer/komplizierter zu realisieren sein könnte als in irgendeinem anderen Framework.

Hauptsache verteidigen? Es geht mir nicht um den Punkt, dass die Frameworks verbreitet sind oder weniger Funktionalität bieten. Aber wenn man Infrastruktur- und Business-Anwendung in einem Guss entwickelen muss, dann wird das Framework eine Nische bleiben.

[ertes]

volkard schrieb:

ertes schrieb:

volkard schrieb:

Vermutlich wieder ist Haskell deutlich "schneller" aber wenn man dann tatsächlich mal nachmißt, ist es hoffnungslos lahm, aber mit "schneller" war in Wirklichkeit schon die ganze Zeit gemeint, daß man den Code schneller eingetippt hat.

Dumme, zusammenhanglose Behauptung. Bleib sachlich oder halt dich einfach raus.

Verzichte doch einfach auf die unpassenden Seitenhiebe gegen C++.
http://shootout.alioth.debian.org/u64q/benchmark.php?test=binarytrees&lang=all

Wenn ich mir den entsprechenden Haskell-Code anschaue, wundert mich das Ergebnis nicht. Mich würde derselbe Benchmark mit Data.IntSet interessieren. Dass eine schlechte Haskell-Implementierung nicht schneller als eine optimierte C++-Implementierung ist, kann ich nachvollziehen. Um optimierte Datenstrukturen in Haskell zu implementieren, sollte man die Sprachsemantik erst mal verstanden haben. Die Art, auf die der Baum im Shootout in Haskell implementiert wurde, bedeutet, dass für jede verändernde Operation der gesamte Baum kopiert werden muss. Das verraten schon die Ausrufezeichen in dieser Zeile:

data Tree = Nil | Node !Int !Tree !Tree

Der Shootout ist eben kein Sprachvergleich, sondern ein Implementierungsvergleich. So. Was hat jetzt dein Link für einen Inhalt gehabt? Keinen.

Zeus schrieb:

Hauptsache verteidigen?

Ich denke, ich bin hier einer der Wenigen, die stets objektiv bleiben. Wenn du den Thread verfolgt hast, wirst du festgestellt haben, dass ich Haskell (oder Racket oder was auch immer) durchaus nicht in jeder Hinsicht verteidigt habe.

Es geht mir nicht um den Punkt, dass die Frameworks verbreitet sind oder weniger Funktionalität bieten. Aber wenn man Infrastruktur- und Business-Anwendung in einem Guss entwickelen muss, dann wird das Framework eine Nische bleiben.

Sie werden nicht viel genutzt werden, da es eben immer noch Haskell/Racket ist. Das sagt aber nichts über die Frameworks als Solche aus. Das war meine Aussage. Nicht mehr, nicht weniger.

[currywurst]

ertes schrieb:

Aber ich denke, ich nehme mir auch so genug Zeit für das Forum hier.

Ich habe mir die Zeit genommen, den Thread durchzulesen und mich hast du davon überzeugt, Haskell zu lernen. Vielen Dank dafür!

[otze]

ertes schrieb:

data Tree = Nil | Node !Int !Tree !Tree

Der Shootout ist eben kein Sprachvergleich, sondern ein Implementierungsvergleich. So. Was hat jetzt dein Link für einen Inhalt gehabt? Keinen.

Das ganze wird in dem Moment ein Sprachvergleich, sobald kein Programmeirer mehr in de rLage ist, in den jeweiligen Sprachen ein schnelleres Programm zu erzeugen. Also, wenn du dich darüber beschweren kannst, kannst du als Haskell Jünger doch sicher ein schnelleres Programm erzeugen.

[CStoll]

ertes schrieb:

CStoll schrieb:

OK, wir haben eine Funktion sqrt(), die nur positive Zahlen als Parameter entgegennimmt, eine Funktion arcsin(), die nur Zahlen im Bereich [-1,1] akzeptiert und einige weitere die auch ihre jeweiligen Einschränkungen haben. Und aus diesen Funktionen wollen wir nun komplexere Funktionen zusammenbauen (z.B. die pq-Formel für quadratische Gleichungen). Allerdings kannst du bei den meisten Funktionen nicht garantieren, daß ihre Werte in einem bestimmten Bereich bleiben, d.h. du mußt die zusammengesetzte Funktion mit Fallunterscheidungen spicken, um die Wertebeschränkungen sicherzustellen.

Nein, die Funktionen kannst du zusammensetzen, wie du willst, solange die Typen passen. Es kommt auf die Werte an, die in das System geschickt werden. Aber ist auch egal, denn sowas zu bewerkstelligen ist in Haskell zu aufwendig, um praktikabel sein. Ich sage es jetzt zum letzten mal und werde dann auch nicht weiter auf das Thema eingehen: Haskell ist nicht dafür geeignet, numerische Korrektheit von Formeln zu beweisen. Es ist möglich, aber viel zu aufwendig. Schau dir Agda und Coq an, wenn dich das Thema interessiert. Thema ist meinerseits beendet.

Du hast mir immer noch nicht verraten, welchen Typ und welche Definition eine Subtraktionsmethode haben muß, um vom Compiler sicherstellen zu lassen, daß der Ausdruck "sqrt(x-y)" immer gültige Werte erhält.

Du hast einige Begriffe in den Raum geworfen.

Nun, ich traue den meisten hier zu, eine Suchmaschine richtig zu benutzen. Aber ich habe auch schon Links gepostet. Du wolltest z.B. praktischen, produktiven Code sehen. Ich habe dir welchen verlinkt. Plötzlich gings du überhaupt nicht mehr darauf ein. Du gehst nur auf die Themen ein, in denen du vermutest, dass du mir widersprechen und/oder Haskell in den Boden stampfen kannst. Hat es dich so erschreckt, dass richtige Real World-Bibliotheken in Haskell gibt, und dass man mit denen tatsächlich produktiv arbeiten kann?

Wenn ich z.B. den Begriff GADT an Google verfüttere, bekomme ich einiges, wa aber entweder nichts mit Haskell zu tun hat oder für einen Außenstehenden völlig unverständlich ist. Das Konzept von Phantomtypen kann man damit eventuell verstehen, aber wie diese mit den reellen Typen interagieren ist nicht wirklich klar.
(du kannst ja gerne deinen Code posten, mit dem du Sortiertheit bewiesen hast)

Das letzte, was du verlinkt hast, war der Artikel über das "Blub-Paradoxon".

Und eventuell solltest du meine Bemerkungen auch zu Ende lesen. Klar kannst du deine Typen und Funktionen so weit einschränken, daß sie nur auf eine bestimmte Art verwendet werden können, aber was für einen Sinn macht das? Und solange die beteiligten Ausdrücke mit den selben Typen zusammenpassen, wird dein Compiler keinen Unterschied bemerken.

So ist es. Und wenn du den Sinn darin nicht siehst, dann hat es keinen Wert, darüber zu diskutieren. Du kannst in Haskell viele statische Garantien erreichen, die in C++ undenkbar sind, aber es hat keinen Wert, dir das näherzubringen. Einerseits bist du versteift in deiner Überzeugung, andererseits bist du aber nicht bereit, Haskell erst mal wirklich auszuprobieren, bevor du urteilst.

Wenn ich wirklich Wert darauf legen würde, könnte ich auch zwei Dutzend Hilfstypen definieren und passende Funktionen definieren, so daß es genau EINE legale Reihenfolge gibt, diese Typen zusammenzufassen. Das hindert mich aber in C++ genausowenig wie in Haskell daran, die verwendeten Werte ans Limit auszureizen.

Wie schon gesagt: Ich kenne C++ und Haskell, beide aus mehrjähriger Erfahrung. Du kennst nur C++ und zeigst keine Bereitschaft, das zu ändern. Somit ist die ganze Diskussion, die wir führen, Zeitverschwendung.

Ich hatte während des Studiums kurze Berührungspunkte mit Haskell, aber es danach nicht wieder gebraucht. Inzwischen muß ich mit dem auskommen, was mein Arbeitgeber nutzt (nein, das ist nicht C++, sondern schlimmer).
Und ich bin durchaus bereit zuzugeben, daß Haskell seine Vorteile hat, aber es hat auch Schwächen - und vor allem habe ich bislang immer noch gehofft, konstruktive Argumente von dir zu hören anstatt plumber Schlagworte.

Bitte schön, hier der Haskell-Code dazu: […]

Und wie sieht der in der Anwendung aus?

Nicht anders als bei entsprechenden C/C++/Ruby/Smalltalk-Bibliotheken, außer dass diese Bibliothek effektfrei ist. Beispiel:

newHeaders = M.insert "Content-type" "text/plain" oldHeaders

Wenn man seinen Code richtig funktional schreibt, sieht man da aber meistens nur entweder auf der rechten oder auf der linken Seite einen Namen, etwa wenn man mit StateT arbeitet: modify (M.insert "Content-type" "text/plain") .

(PS: eine vorgefertigte Library zu verwenden ist keine Kunst - das geht in C++ genauso einfach)

Wenn du deine import-Anweisung als vollwertiges Programm ansiehst, das geht im C++ übrigens genauso schnell:

#include <map>

Und übrigens ist dein Anwendungsbeispiel alles andere als typsicher.

[!rr!rr_.]

Wenn du deine import-Anweisung als vollwertiges Programm ansiehst, das geht im C++ übrigens genauso schnell:

#include <map>

so lang .. ? in smalltalk geht das kürzer:

kein Witz - Dictionaries sind für gewöhnlich schon out-of-the-box in der Klassenhierarchie im Image.

[ertes]

currywurst schrieb:

Ich habe mir die Zeit genommen, den Thread durchzulesen und mich hast du davon überzeugt, Haskell zu lernen. Vielen Dank dafür!

Gerne, aber nimm viel Zeit mit.

otze schrieb:

Das ganze wird in dem Moment ein Sprachvergleich, sobald kein Programmeirer mehr in de rLage ist, in den jeweiligen Sprachen ein schnelleres Programm zu erzeugen. Also, wenn du dich darüber beschweren kannst, kannst du als Haskell Jünger doch sicher ein schnelleres Programm erzeugen.

Natürlich. Es hat schließlich kein Haskell-Programmierer etwas Besseres zu tun als den ganzen Tag im Shootout irgendwelchen C++-Fanatikern irgendwas zu beweisen. Gute C++-Programmierer gibt es im Vergleich zu guten Haskell-Programmierern wie Sand am Meer. Die Handvoll der Letzteren, die es gibt, scheren sich einen Dreck um deine oder volkards Meinung.

CStoll schrieb:

Wenn ich z.B. den Begriff GADT an Google verfüttere, bekomme ich einiges, wa aber entweder nichts mit Haskell zu tun hat oder für einen Außenstehenden völlig unverständlich ist. Das Konzept von Phantomtypen kann man damit eventuell verstehen, aber wie diese mit den reellen Typen interagieren ist nicht wirklich klar.

Natürlich kannst du GADTs nicht verstehen, wenn du das Typensystem von Haskell nicht verstehst. Phantomtypen, oder eigentlich eher Phantomtypparameter, sind nichts Besonderes. Das sind einfach nur Parameter eines Typs, die keine Laufzeitfunktion haben. Das heißt, es existieren zur Laufzeit keine konkreten Werte dieses Typs. Mit GADTs haben Phantomtypen nicht viel zu tun, aber sie werden gerne kombiniert.

Das letzte, was du verlinkt hast, war der Artikel über das "Blub-Paradoxon".

Falsch. Den solltest du dir aber dennoch durchlesen. Du leidest nämlich im Moment an genau diesem Paradoxon, so wie viele andere hier.

Ich hatte während des Studiums kurze Berührungspunkte mit Haskell, aber es danach nicht wieder gebraucht. Inzwischen muß ich mit dem auskommen, was mein Arbeitgeber nutzt (nein, das ist nicht C++, sondern schlimmer).
Und ich bin durchaus bereit zuzugeben, daß Haskell seine Vorteile hat, aber es hat auch Schwächen - und vor allem habe ich bislang immer noch gehofft, konstruktive Argumente von dir zu hören anstatt plumber Schlagworte.

Ich habe konstruktive Argumente geliefert, aber es bringt nichts, wenn du mit ihnen nichts anfangen kannst. Vieles von dem, was ich schreibe, kannst du doch gar nicht nachvollziehen, ohne Haskell zu kennen. Wenn du bereit bist, Haskell richtig zu lernen, bin ich auch gerne wieder bereit, mit dir über statische Garantien zu diskutieren. Vorher musst du aber die Basics können, denn sonst ist die Diskussion für mich einfach nur ermüdend und macht keinen Spaß. Ich poste dir proof of concept-Code, du widersprichst trotzdem, weil das in deinen C++-Verstand einfach nicht reingeht. Deswegen gehe ich vorerst – wie angekündigt – auch konsequent auf nichts mehr ein, was mit diesem Thema zu tun hat.

Wenn du deine import-Anweisung als vollwertiges Programm ansiehst, das geht im C++ übrigens genauso schnell:

#include <map>

Und übrigens ist dein Anwendungsbeispiel alles andere als typsicher.

Ja? Vielleicht möchtest du diese Behauptung mit Argumenten oder Beispielen untermauern.

[CStoll]

ertes schrieb:

CStoll schrieb:

Wenn ich z.B. den Begriff GADT an Google verfüttere, bekomme ich einiges, wa aber entweder nichts mit Haskell zu tun hat oder für einen Außenstehenden völlig unverständlich ist. Das Konzept von Phantomtypen kann man damit eventuell verstehen, aber wie diese mit den reellen Typen interagieren ist nicht wirklich klar.

Natürlich kannst du GADTs nicht verstehen, wenn du das Typensystem von Haskell nicht verstehst. Phantomtypen, oder eigentlich eher Phantomtypparameter, sind nichts Besonderes. Das sind einfach nur Parameter eines Typs, die keine Laufzeitfunktion haben. Das heißt, es existieren zur Laufzeit keine konkreten Werte dieses Typs. Mit GADTs haben Phantomtypen nicht viel zu tun, aber sie werden gerne kombiniert.

Dann erklär's mir doch mal an einem praktischen Beispiel - bei den arithmetischen Funktionen hast du schließlich schon wieder einen Rückzieher gemacht.

Das letzte, was du verlinkt hast, war der Artikel über das "Blub-Paradoxon".

Falsch. Den solltest du dir aber dennoch durchlesen. Du leidest nämlich im Moment an genau diesem Paradoxon, so wie viele andere hier.

Was dann? Wenn du nicht ein Doppelgänger von knivil oder volkard bist (was ich mal nicht hoffe), war das hier der letzte Beitrag, wo du etwas verlinkt hast.

Ich habe konstruktive Argumente geliefert, aber es bringt nichts, wenn du mit ihnen nichts anfangen kannst. Vieles von dem, was ich schreibe, kannst du doch gar nicht nachvollziehen, ohne Haskell zu kennen. Wenn du bereit bist, Haskell richtig zu lernen, bin ich auch gerne wieder bereit, mit dir über statische Garantien zu diskutieren. Vorher musst du aber die Basics können, denn sonst ist die Diskussion für mich einfach nur ermüdend und macht keinen Spaß. Ich poste dir proof of concept-Code, du widersprichst trotzdem, weil das in deinen C++-Verstand einfach nicht reingeht. Deswegen gehe ich vorerst – wie angekündigt – auch konsequent auf nichts mehr ein, was mit diesem Thema zu tun hat.

Du postest Fragmente und wenn dich jemand um Details oder Ergänzungen bittet, tust du es mit einem "kann man machen" ab. Und mit deinen Ergüssen hast du bei mir (leider) das genaue Gegenteil erreicht wie bei currywurst. Ich hoffe, bei unserer nächsten Begegnung geht es um etwas, wo du eher gesprächsbereit bist.

PS: Und kein System der Welt kann dir Garantien bieten, die mathematisch nicht realisierbar sind.

[!rr!rr_.]

man fragt sich, ob Typsicherheit überhaupt diesen unglaublichen Aufwand wert ist.

Ich kann mich jedenfalls nicht erinnern, wann ich zuletzt einen Typfehler bei der Programmierung mit einer dynamisch typisierten Programmiersprache hatte - in den letzten 4 Jahren mit Sicherheit kein einziges Mal.

Und selbst wenn, dann kann man diese Gefahr (und viele andere mögliche Fehlerquellen) minimieren durch sprechende Bezeichner und vor allem durch feinkörnige Unit-Tests, die synchron mit dem Sourcecode aufgebaut werden.

[GPC]

!rr!rr_. schrieb:

man fragt sich, ob Typsicherheit überhaupt diesen unglaublichen Aufwand wert ist.

Ich kann mich jedenfalls nicht erinnern, wann ich zuletzt einen Typfehler bei der Programmierung mit einer dynamisch typisierten Programmiersprache hatte - in den letzten 4 Jahren mit Sicherheit kein einziges Mal.

Und selbst wenn, dann kann man diese Gefahr (und viele andere mögliche Fehlerquellen) minimieren durch sprechende Bezeichner und vor allem durch feinkörnige Unit-Tests, die synchron mit dem Sourcecode aufgebaut werden.

Ack. Statische Typisierung ist zwar ganz nett, um die gröbsten Fehler rauszuhalten und den Programmierer vor sich selbst zu schützen, aber ansonsten find ich's eher lächerlich, wie da manche drauf abgehen, als sei es das Allheilmittel der Programmierung

[hustbaer]

!rr!rr_. schrieb:

Wenn du deine import-Anweisung als vollwertiges Programm ansiehst, das geht im C++ übrigens genauso schnell:

#include <map>

so lang .. ? in smalltalk geht das kürzer:

kein Witz - Dictionaries sind für gewöhnlich schon out-of-the-box in der Klassenhierarchie im Image.

So lang ...? Einen gleichwertigen Beitrag zur Diskussion kann ich so machen:

Kein Witz - deine Beiträge sind für gewöhnlich ausser sinnlos nur noch sinnlos.

[ertes]

CStoll schrieb:

Dann erklär's mir doch mal an einem praktischen Beispiel - […]

Eine Standardanwendung für GADTs findest du an jeder Ecke im Netz: Eine EDSL für eine kleine Arithmetik-Sprache. Such selber. Ich habe keine Lust mehr.

bei den arithmetischen Funktionen hast du schließlich schon wieder einen Rückzieher gemacht.

Nö, hab ich nicht.

Was dann? Wenn du nicht ein Doppelgänger von knivil oder volkard bist (was ich mal nicht hoffe), war das hier der letzte Beitrag, wo du etwas verlinkt hast.

Okay, dann möge es so sein.

Du postest Fragmente und wenn dich jemand um Details oder Ergänzungen bittet, tust du es mit einem "kann man machen" ab. Und mit deinen Ergüssen hast du bei mir (leider) das genaue Gegenteil erreicht wie bei currywurst. Ich hoffe, bei unserer nächsten Begegnung geht es um etwas, wo du eher gesprächsbereit bist.

Denkst du eigentlich, ich habe ewig Zeit? Wenn du wirklich Interesse an Haskell hast, dann hörst du auf mich, wenn ich dir fünfhundert mal sage:

HALLO, KANNST DU LESEN ODER WAS? HASKELL IST DAFÜR NICHT GEEIGNET!

Entweder du bist wirklich strohdumm, oder du willst mich einfach nur ärgern. Nochmal zum Mitschreiben:

HASKELL IST DAFÜR NICHT GEEIGNET!

Wie oft noch? Ich sage dir hundert mal, dass es sehr schwierig und aufwendig ist, und du erwartest immer noch von mir, dass ich mir die Mühe mache, stundenlang Code für dich zu schreiben, nur um dich von irgendwas zu überzeugen. Offenbar bist du unfähig, direkte Aussagen in deine Birne reinzubekommen. Und wenn du nicht damit aufhörst, dann antworte ich dir gar nicht mehr. Außerdem würde dasselbe Argument genauso auch gegen C++ sprechen, sogar noch viel mehr als gegen Haskell, wie du ja schon selber zugegeben hast. Aber es ist mir egal, ob dir die Sprache gefällt oder nicht. Du hattest eine Frage, und ich habe sie ernstgenommen. Und wenn du das hier nur machst, um mir auf die Nerven zu gehen, dann finde ich das wirklich schade.

Zurück zu dem, was ich wirklich gesagt habe; ich habe in diesem Thread genau drei Behauptungen über Haskell aufgestellt, zumindest im Kern meiner Aussagen:

• Haskell ist typensicher und Programme, die kompilieren, funktionieren meistens auch. Viele Bugs, die in C++ erst zur Laufzeit auftreten würden, fängt in Haskell bereits der Compiler ab. (Eure Interpretation: Ich würde meine Programme nie testen. Ich würde meine Programme so schreiben, dass jede noch so kleine Kleinigkeit statisch garantiert wird.)
• Haskell ist besser als C++ für Serverprogramme und Webanwendungen. (Darauf ist bisher keiner richtig eingegangen. Offenbar habe ich da wohl eine echte Schwachstelle von C++ erwischt.)
• Haskell muss sich performancemäßig schon lange nicht mehr vor C++ verstecken. (Als Gegenargument bekam ich lediglich einen Shootout-Link, in dem eine schlechte Haskell-Implementierung gegen eine gute C++-Implementierung antritt.)

Niemand konnte bisher schlagende Argumente dagegen bieten. Haskell ist weiterhin besser für Serverprogramme und Webanwendungen. Haskell ist weiterhin sicherer als C++. Und auch wenn Haskell-Code in Micro-Benchmarks nicht schneller als C++-Code läuft: Die Performance ist vergleichbar oder für praktische Zwecke nur unwesentlich langsamer, teilweise aber auch schneller. Gerade im Bereich der konkurrenten Programmierung schlägt Haskell C++ nieder in jeder Hinsicht. Und wenn ihr gegenargumentieren wollt, dann tut das bitte mit Code. Ich habe bereits Code geliefert.

PS: Und kein System der Welt kann dir Garantien bieten, die mathematisch nicht realisierbar sind.

Von solchen Garantien war auch keine Rede. Aber bedenke, dass einige Garantien nur deshalb nicht möglich sind, weil du in Turing-Maschinen denkst. Ich habe dich diesbezüglich (auch schon wieder mehrfach) auf Agda hingewiesen, eine Sprache, die genau aus diesem Grund nicht turingvollständig ist.

!rr!rr_. schrieb:

man fragt sich, ob Typsicherheit überhaupt diesen unglaublichen Aufwand wert ist.

Welchen Aufwand denn? Vergiss mal, was CStoll schreibt. Der redet nicht von Typsicherheit, sondern von mathematischen Beweisen. Das hat nichts mit praktischer Typensicherheit zu tun, und ist in Haskell prinzipiell auch nicht gut lösbar. Dafür braucht man einen Beweisassistenten wie Agda oder Coq.

Ich kann mich jedenfalls nicht erinnern, wann ich zuletzt einen Typfehler bei der Programmierung mit einer dynamisch typisierten Programmiersprache hatte - in den letzten 4 Jahren mit Sicherheit kein einziges Mal.

Dynamisch ist das eine, schwach ist das andere. Python etwa hat, so weit ich weiß, ein dynamisches und dennoch starkes Typensystem. Außerdem musst du bedenken, dass in den meisten Sprachen nur die Datentypen im Typensystem ausgedrückt werden. In Haskell wird aber auch ein Großteil der Programmlogik in Typen ausgedrückt. Das heißt, viele Fehler in deiner Programmlogik sind in Haskell Typenfehler. Kombiniert mit der Tatsache, dass Haskell ein statisches, starkes Typensystem hat, bedeutet das, dass viele Logikfehler bereits zur Kompilierzeit abgefangen werden.

Und selbst wenn, dann kann man diese Gefahr (und viele andere mögliche Fehlerquellen) minimieren durch sprechende Bezeichner und vor allem durch feinkörnige Unit-Tests, die synchron mit dem Sourcecode aufgebaut werden.

Oder durch eine Spezifikation. Unit-Tests schreibe ich meistens für numerischen Code. Einen Primzahltest etwa würde ich durch einen Unit-Test jagen.

[ipsec]

Wo du gerade nochmal Agda erwähnst. Du sagst (sinngemäß) Agda ist nicht turingvollständig, weil Endlosschleifen nicht möglich sind, trotzdem sind endlose Programme durch Corekursionen möglich. Für mich ist das ein Widerspruch. Wenn es nicht turingvollständig ist, kann man damit nicht alle Programme schreiben (wie praktisch relevant diese Beschränkung auch immer sein möge). Wenn man solche Programme jetzt doch schreiben kann, ist es doch turingvollständig.

[volkard]

ertes schrieb:

Haskell ist weiterhin sicherer als C++. Und auch wenn Haskell-Code in Micro-Benchmarks nicht schneller als C++-Code läuft: Die Performance ist vergleichbar oder für praktische Zwecke nur unwesentlich langsamer, teilweise aber auch schneller. Gerade im Bereich der konkurrenten Programmierung schlägt Haskell C++ nieder in jeder Hinsicht.

Ach, ist doch Quatsch, was Du da erzählst.

[audacia]

CStoll schrieb:

PS: Und kein System der Welt kann dir Garantien bieten, die mathematisch nicht realisierbar sind.

Eben. Warum reitest du dann darauf herum?

!rr!rr_. schrieb:

Ich kann mich jedenfalls nicht erinnern, wann ich zuletzt einen Typfehler bei der Programmierung mit einer dynamisch typisierten Programmiersprache hatte - in den letzten 4 Jahren mit Sicherheit kein einziges Mal.

Und selbst wenn, dann kann man diese Gefahr (und viele andere mögliche Fehlerquellen) minimieren durch sprechende Bezeichner und vor allem durch feinkörnige Unit-Tests, die synchron mit dem Sourcecode aufgebaut werden.

Ich weiß nicht, mit welchen dynamisch typisierten Sprachen du so arbeitest; bei mir waren es zuletzt PHP und R, und obgleich ich die Vorteile durchaus sehe - in R hatte ich meinen Spaß damit, die gängigen arithmetischen Operatoren derart zu überschreiben, daß man sie zwecks point-free-Formulierung auch auf Funktionen anwenden kann -, muß ich eigentlich jedes Mal in der Dokumentation nachschauen, welche Datentypen die Funktion nun wirklich behandeln kann, auch wenn mir völlig klar war, was die Funktion tut. In einer statisch typisierten Sprache reicht es, den Parameter-Tooltip der IDE anzustarren.

Gerade in R kann man mit der unscharfen Trennung zwischen Skalaren und Vektoren viel Mist bauen. Die Sprache erlaubt etwa a * b für beliebige Kombinationen von Vektoren und Skalaren. Haben a und b die gleiche Anzahl Einträge, wird der Operator elementweise angewandt; ist einer davon skalar, so ist es eine skalare Multiplikation. Das ist sehr praktisch, weil ich dann den RMS eines Vektors x mit sqrt(sum(x^2)/length(x)) ausrechnen kann. Ist aber length(a) != length(b) && length(a) != 1 && length(b) != 1 , so gibt es einen Laufzeitfehler, weil R nicht weiß, was es tun soll. Das ist besonders lustig in Verbindung mit den Plot-Funktionen; wenn ich plot(sin) mache, übergibt plot() nicht etwa Skalare, sondern einen Vektor an sin() und erwartet, daß sin() sich selbst elementweise darauf anwendet. Bei sin() klappt das auch, aber bei etwas filigraneren selbstgeschriebenen Funktionen eben oft nicht.

Dergleichen Wildwuchs kenne ich aus allen dynamisch typisierten Sprachen, die mir begegnet sind. Besonders die Unsitte, daß man, anstelle eine Eigenschaft zu spezifizieren, auch einfach ein Objekt übergeben kann, das diese Eigenschaft hat - das macht den Code unleserlich, führt zu Verwirrung, weil es meist nur in bestimmten Situationen geht, und verursacht oft abenteuerliche Laufzeitfehlermeldungen.

ertes schrieb:

Haskell ist besser als C++ für Serverprogramme und Webanwendungen. (Darauf ist bisher keiner richtig eingegangen. Offenbar habe ich da wohl eine echte Schwachstelle von C++ erwischt.)

Ungefähr niemand macht Webentwicklung in C++; warum sollte man auch. Praktisch jeder benutzt ASP.NET oder PHP, Ausnahmen bestätigen die Regel.

ipsec schrieb:

Wo du gerade nochmal Agda erwähnst. Du sagst (sinngemäß) Agda ist nicht turingvollständig, weil Endlosschleifen nicht möglich sind, trotzdem sind endlose Programme durch Corekursionen möglich. Für mich ist das ein Widerspruch. Wenn es nicht turingvollständig ist, kann man damit nicht alle Programme schreiben (wie praktisch relevant diese Beschränkung auch immer sein möge). Wenn man solche Programme jetzt doch schreiben kann, ist es doch turingvollständig.

Ich weiß nicht, was ertes da sagen wollte, aber ein Programm muß nicht turingvollständig sein, nur weil es nicht terminiert.

[CStoll]

ertes schrieb:

CStoll schrieb:

Dann erklär's mir doch mal an einem praktischen Beispiel - […]

Eine Standardanwendung für GADTs findest du an jeder Ecke im Netz: Eine EDSL für eine kleine Arithmetik-Sprache. Such selber. Ich habe keine Lust mehr.

bei den arithmetischen Funktionen hast du schließlich schon wieder einen Rückzieher gemacht.

Nö, hab ich nicht.

Wo ist dann die Erkläung, wie man Subtraktion und Wurzel typsicher miteinander kombinieren kann. Du hast zwar behauptet, daß das ohne Laufzeitpüfungen geht, aber den Beweis hast du unterschlagen.

Du postest Fragmente und wenn dich jemand um Details oder Ergänzungen bittet, tust du es mit einem "kann man machen" ab. Und mit deinen Ergüssen hast du bei mir (leider) das genaue Gegenteil erreicht wie bei currywurst. Ich hoffe, bei unserer nächsten Begegnung geht es um etwas, wo du eher gesprächsbereit bist.

Denkst du eigentlich, ich habe ewig Zeit? Wenn du wirklich Interesse an Haskell hast, dann hörst du auf mich, wenn ich dir fünfhundert mal sage:

HALLO, KANNST DU LESEN ODER WAS? HASKELL IST DAFÜR NICHT GEEIGNET!

Du bemerkst anscheinend gar nicht, wie du dir selber widerspichst. Auf der einen Seite sagst du, daß Haskell typische C++ Fehler zur Compilezeit abfangen kann, auf der anderen Seite kommt dann

HASKELL IST DAFÜR NICHT GEEIGNET!

Haskell ist typensicher und Programme, die kompilieren, funktionieren meistens auch. Viele Bugs, die in C++ erst zur Laufzeit auftreten würden, fängt in Haskell bereits der Compiler ab. (Eure Interpretation: Ich würde meine Programme nie testen. Ich würde meine Programme so schreiben, dass jede noch so kleine Kleinigkeit statisch garantiert wird.)

Das liegt aber nur daran, daß Haskell viele Aspekte hinter den Kulissen abwickelt, die der C++ Entwickler direkte beeinflussen kann.
Außerdem kannst du die falsche Verwendung von Datenypen in C++ genauso unterbinden wie in Haskell (ist nur ein wenig aufwendiger, aber machbar). Die meisten Laufzeitfehler, die mir in letzter Zeit untergekommen sind, basierten auf Rechen- oder Denkfehlern und Daten, die erst zur Laufzeit bekannt sind. Sowas kannst du nicht diagnostizieren indem du es in ein Typ-Korsett presst.

Haskell ist besser als C++ für Serverprogramme und Webanwendungen. (Darauf ist bisher keiner richtig eingegangen. Offenbar habe ich da wohl eine echte Schwachstelle von C++ erwischt.)

Web-Anwendungen sind ja auch nicht das Spezialgebiet von C++, dafü gibt es genug andere Sprachen, mit denen du dich vergleichen könntest.

Haskell muss sich performancemäßig schon lange nicht mehr vor C++ verstecken. (Als Gegenargument bekam ich lediglich einen Shootout-Link, in dem eine schlechte Haskell-Implementierung gegen eine gute C++-Implementierung antritt.)

Ich hab' den Shootout jetzt nicht im Detail analysiert, aber woher willst du wissen, wie gut die einzelnen Kandidaten tatsächlich optimiert worden sind?

Von solchen Garantien war auch keine Rede. Aber bedenke, dass einige Garantien nur deshalb nicht möglich sind, weil du in Turing-Maschinen denkst. Ich habe dich diesbezüglich (auch schon wieder mehrfach) auf Agda hingewiesen, eine Sprache, die genau aus diesem Grund nicht turingvollständig ist.

Klar, wenn man die Möglichkeiten einer Sprache einschränkt, kann man innerhalb dieser Möglichkeiten irgendwann alles beweisen. Das Problem ist, daß du mit einer solchen Sprache schneller an die Grenzen dessen kommst, was du darstellen kannst.
(Oder habe ich die Entdeckung von etwas verpasst, was echt mächtiger ist als eine Turing-Maschine?)

!rr!rr_. schrieb:

man fragt sich, ob Typsicherheit überhaupt diesen unglaublichen Aufwand wert ist.

Welchen Aufwand denn? Vergiss mal, was CStoll schreibt. Der redet nicht von Typsicherheit, sondern von mathematischen Beweisen. Das hat nichts mit praktischer Typensicherheit zu tun, und ist in Haskell prinzipiell auch nicht gut lösbar. Dafür braucht man einen Beweisassistenten wie Agda oder Coq.

Du wolltest doch Fehlerfreiheit durch Typsicherheit ausdrücken (oder war das einer der anderen Haskell-Anhänger - jedenfalls kam von einem von euch die Aussage "wenn es sich compilieren lässt, ist es fehlerfrei"?).

[volkard]

ertes schrieb:

Haskell ist typensicher und Programme, die kompilieren, funktionieren meistens auch. Viele Bugs, die in C++ erst zur Laufzeit auftreten würden, fängt in Haskell bereits der Compiler ab. (Eure Interpretation: Ich würde meine Programme nie testen. Ich würde meine Programme so schreiben, dass jede noch so kleine Kleinigkeit statisch garantiert wird.)

Das rührt aus einem Mißverständnis her.
Jeder, der "Effektiv C++ programmieren" gelesen und verstanden hat, macht auch in C++ viele Bugs, die in vielen anderen Sprachen erst zur Laufzeit auftreten würden, zu Compilerfehlern. Wir versuchten zu ergründen, was Haskell da an Mehrwert hat. Und Du bliebst für uns enorm schwammig widersprüchlich leer, weil Du einerseits Codebeispiele gezeigt hast, die dann doch zu extrem waren und Du sie selber nicht verwendest, und andererseits Codebeispiele zeigtest, die verwendbar sind und auch in modernem C++ eine Selbstverständlichkeit sind. Es war kein Mehrwert ersichtlich, obwohl Du dauernd den Mehrwert betont hast. Verwirrend. Also fragt man nach. Und es kommt nur weiter *******.
Wir gingen dummerweise davon aus, daß Du C++ total gut kannst. Weil Du es mehrfach behauptet hast. Ab jetzt spreche ich es auch Dir ab. Es gibt viele mehrjährige C++-Programmierer, die nicht gut sind. Es würde einfach gut erklären, warum Du Dich in Haskell so verknallt hast. Fröhliche Ostern!

[volkard]

CStoll schrieb:

Die meisten Laufzeitfehler, die mir in letzter Zeit untergekommen sind, basierten auf Rechen- oder Denkfehlern und Daten, die erst zur Laufzeit bekannt sind. Sowas kannst du nicht diagnostizieren indem du es in ein Typ-Korsett presst.

Es kann sich lohnen, "typische" Fehler durchs Typsystem zu verbieten. Ich stelle mir als Beispiel vor, daß man so erzwingt, daß socket::bind aufgerufen wird. Erspart einem auch den Blick ins Handbuch.
Das Korsett kann ich allerdings erst basteln, wenn ich das richtige Vorgehen herausgefunden habe.
Aber kaum der Rede wert. Die Arbeitszeitfreßfehler tauchen dort gar nicht auf.

[ertes]

ipsec schrieb:

Wo du gerade nochmal Agda erwähnst. Du sagst (sinngemäß) Agda ist nicht turingvollständig, weil Endlosschleifen nicht möglich sind, trotzdem sind endlose Programme durch Corekursionen möglich. Für mich ist das ein Widerspruch. Wenn es nicht turingvollständig ist, kann man damit nicht alle Programme schreiben (wie praktisch relevant diese Beschränkung auch immer sein möge). Wenn man solche Programme jetzt doch schreiben kann, ist es doch turingvollständig.

Das bedeutet nur, dass man dennoch Programme schreiben kann, die unendlich lange laufen. Die Sprache wird deshalb aber nicht turingvollständig. Das Halteproblem etwa existiert in Agda nicht. Du kannst einen Algorithmus schreiben, der sagen kann, wann ein Agda-Programm terminiert. Zwei mögliche Ausgaben des Programms sind etwa, dass das Programm immer terminiert, oder dass es terminiert, sobald der Benutzer die "q"-Taste gedrückt hat. So ein Programm kannst du für eine turingvollständige Sprache nicht schreiben.

audacia schrieb:

ertes schrieb:

Haskell ist besser als C++ für Serverprogramme und Webanwendungen. (Darauf ist bisher keiner richtig eingegangen. Offenbar habe ich da wohl eine echte Schwachstelle von C++ erwischt.)

Ungefähr niemand macht Webentwicklung in C++; warum sollte man auch. Praktisch jeder benutzt ASP.NET oder PHP, Ausnahmen bestätigen die Regel.

Aber Server-Programmierung wird doch in C++ gemacht, oder irre ich mich? Und Webentwicklung macht niemand in C++, weil es so ungeheuer schwierig ist. Da fängt es ja schon damit an, dass es kaum brauchbare Bibliotheken dafür gibt, ganz zu schweigen von einem richtigen Framework.

CStoll schrieb:

bei den arithmetischen Funktionen hast du schließlich schon wieder einen Rückzieher gemacht.

Nö, hab ich nicht.

Wo ist dann die Erkläung, wie man Subtraktion und Wurzel typsicher miteinander kombinieren kann. Du hast zwar behauptet, daß das ohne Laufzeitpüfungen geht, aber den Beweis hast du unterschlagen.

Ja, weil ich zufällig auch noch ein Leben habe. Außerdem habe ich die Erklärung gegeben, nur eben ohne Beispielcode. Ich habe einfach Besseres zu tun als eine Stunde lang für dich ein Code-Beispiel auszuarbeiten. Ja, es dauert wirklich so lange, weil Haskell (und jetzt sage ich es schon wieder) nicht dafür geeignet ist. Letzter Beitrag zu dem Thema.

Du bemerkst anscheinend gar nicht, wie du dir selber widerspichst. Auf der einen Seite sagst du, daß Haskell typische C++ Fehler zur Compilezeit abfangen kann, auf der anderen Seite kommt dann

HASKELL IST DAFÜR NICHT GEEIGNET!

Ein typischer C++-Fehler ist für dich, wenn sqrt eine negative Zahl bekommt? Wie es aussieht, bist du in C++ genauso fit wie in Haskell. Also meine häufigsten Fehler in C++ lagen an falschen Schleifen, unüberschaubarer Vererbung, Zeigerprobleme, nicht oder zu früh freigegebene Resourcen, etc.

Das liegt aber nur daran, daß Haskell viele Aspekte hinter den Kulissen abwickelt, die der C++ Entwickler direkte beeinflussen kann.

Da bin ich ja mal gespannt. Zum Beispiel?

Außerdem kannst du die falsche Verwendung von Datenypen in C++ genauso unterbinden wie in Haskell (ist nur ein wenig aufwendiger, aber machbar). Die meisten Laufzeitfehler, die mir in letzter Zeit untergekommen sind, basierten auf Rechen- oder Denkfehlern und Daten, die erst zur Laufzeit bekannt sind. Sowas kannst du nicht diagnostizieren indem du es in ein Typ-Korsett presst.

Datentypen beziehen sich auf Werte. In Haskell fällt aber wesentlich mehr in die Klasse Werte als in C++. Funktionen etwa sind auch Werte und haben einen Typen. Kontrollstrukturen (Schleifen, sofern man sie braucht, Exceptions, sogar Labels und Sprünge) sind normale Werte und haben einen Typen. Die gesamte Programmlogik hat einen Typen. Rechenfehler werden nicht abgefangen, aber Denkfehler, die sich auf die Programmlogik beziehen, sehr wohl. Du hast referentielle Transparenz (Entsprechung in C++ wäre etwa: ist f(x) = 3, dann kannst du überall in deinem Programm den Aufruf f(x) durch das Ergebnis 3 ersetzen, ohne dein Programm zu verändern) und kannst durch lazy evaluation viele Algorithmen auf eine Art schreiben, die den Datenfluss expliziter und deshalb weniger fehleranfällig macht. Wie oft hat man ein falsches Ergebnis, weil man Zuweisungen in der falschen Reihenfolge geschrieben hat?

Ich hab' den Shootout jetzt nicht im Detail analysiert, aber woher willst du wissen, wie gut die einzelnen Kandidaten tatsächlich optimiert worden sind?

Indem ich sie mir ansehe?

Klar, wenn man die Möglichkeiten einer Sprache einschränkt, kann man innerhalb dieser Möglichkeiten irgendwann alles beweisen. Das Problem ist, daß du mit einer solchen Sprache schneller an die Grenzen dessen kommst, was du darstellen kannst.

Also ich weiß nicht. Ein komplettes HTTP-Framework gibt es bereits in Agda. Dieses Framework demonstriert auch schön, wie man in Agda all die schönen Sachen machen kann, die du willst, und die in Haskell nur sehr aufwendig zu realisieren sind.

Du wolltest doch Fehlerfreiheit durch Typsicherheit ausdrücken (oder war das einer der anderen Haskell-Anhänger - jedenfalls kam von einem von euch die Aussage "wenn es sich compilieren lässt, ist es fehlerfrei"?).

Meine Aussage war, dass ein Programm, das kompiliert, in den meisten Fällen auch funktioniert. Ich schreibe meine Programme so, dass ich nur selten Fehler zur Laufzeit finden muss. Und besonders viel Numerik kommt in meinen Programmen nicht vor, daher habe ich auch selten arithmetische Bugs. Die statisch zu prüfen würde aus einem effizienten 1000-Zeilen-Programm ein sehr ineffizientes, kaum zu überblickendes 100000-Zeilen-Programm machen. Das ist auch der Grund, warum ich dir keine Code-Beispiele gebe. Ich nehme mir nicht ein ganzes Wochenende Zeit, nur um dir zu beweisen, dass es möglich ist, auch solche Beweise zu führen.

Außerdem habe ich dir nicht widersprochen, als du sagtest, dass Werte, die von außen reinkommen, auch zur Laufzeit geprüft werden müssen. Diese Prüfung besteht darin, etwa den hereinkommenden String richtig in die Konstruktoren des Datentyps zu verpacken, der den Wert in das statisch geprüfte System nimmt. Dafür brauchst du einen Algorithmus. Wenn dieser Algorithmus etwa eine Benutzereingabe in das x in sqrt(x - 1) einsetzt, dann muss er so geschrieben sein, dass statisch garantiert werden kann, dass x ≥ 1 gilt, ansonsten kompiliert er nicht. Den Aufwand dafür schätze ich auf 500-1000 Zeilen Code mit allem drum und dran. Vielleicht verstehst du jetzt, warum ich dir kein Code-Beispiel gebe, und warum ich ständig immer wieder betone, dass du dir lieber Agda als Haskell anschauen solltest, wenn du sowas willst.

volkard schrieb:

ertes schrieb:

Haskell ist typensicher und Programme, die kompilieren, funktionieren meistens auch. Viele Bugs, die in C++ erst zur Laufzeit auftreten würden, fängt in Haskell bereits der Compiler ab. (Eure Interpretation: Ich würde meine Programme nie testen. Ich würde meine Programme so schreiben, dass jede noch so kleine Kleinigkeit statisch garantiert wird.)

Das rührt aus einem Mißverständnis her.
Jeder, der "Effektiv C++ programmieren" gelesen und verstanden hat, macht auch in C++ viele Bugs, die in vielen anderen Sprachen erst zur Laufzeit auftreten würden, zu Compilerfehlern. Wir versuchten zu ergründen, was Haskell da an Mehrwert hat. Und Du bliebst für uns enorm schwammig widersprüchlich leer, weil Du einerseits Codebeispiele gezeigt hast, die dann doch zu extrem waren und Du sie selber nicht verwendest, und andererseits Codebeispiele zeigtest, die verwendbar sind und auch in modernem C++ eine Selbstverständlichkeit sind. Es war kein Mehrwert ersichtlich, obwohl Du dauernd den Mehrwert betont hast. Verwirrend. Also fragt man nach. Und es kommt nur weiter *******.
Wir gingen dummerweise davon aus, daß Du C++ total gut kannst. Weil Du es mehrfach behauptet hast. Ab jetzt spreche ich es auch Dir ab. Es gibt viele mehrjährige C++-Programmierer, die nicht gut sind. Es würde einfach gut erklären, warum Du Dich in Haskell so verknallt hast. Fröhliche Ostern!

Siehe oben. Nur weil du meine Argumente nicht verstehst, brauchst du nicht mit persönlichen Angriffen loslegen. Das ist übrigens gemeinhin ein Hinweis dafür, dass dir selber die Argumente ausgehen.

[CStoll]

ertes schrieb:

Du bemerkst anscheinend gar nicht, wie du dir selber widerspichst. Auf der einen Seite sagst du, daß Haskell typische C++ Fehler zur Compilezeit abfangen kann, auf der anderen Seite kommt dann

HASKELL IST DAFÜR NICHT GEEIGNET!

Ein typischer C++-Fehler ist für dich, wenn sqrt eine negative Zahl bekommt? Wie es aussieht, bist du in C++ genauso fit wie in Haskell. Also meine häufigsten Fehler in C++ lagen an falschen Schleifen, unüberschaubarer Vererbung, Zeigerprobleme, nicht oder zu früh freigegebene Resourcen, etc.

Das liegt aber nur daran, daß Haskell viele Aspekte hinter den Kulissen abwickelt, die der C++ Entwickler direkte beeinflussen kann.

Da bin ich ja mal gespannt. Zum Beispiel?

Die Beispiele hast du doch selber gerade genannt: In C++ kann man direkt mit dem Speicher hantieren, muß dann aber mit den Konsequenzen umgehen können. In C++ kann man seine Daten auch in vernünftige Container packen, die einem derartige Probleme dann abnehmen. In Haskell hast du den Vorteil, daß du von Haus aus von der Low-Level Speicherverwaltung abgekoppelt bist und sich schon ein schlauer Compiler-Entwickler um deren Risiken gekümmert hat.

Um mal weg von der Arithmetik zu kommen (ist dir wohl ohnehin zu abstrakt), ein typischeres Problem in C++ sind ungültige Indizes. Ich kann in beiden Sprachen eine Funktion schreiben, die mir das n-te Element einer Liste liefert - und die werden in beiden Sprachen Probleme bekommen, wenn ich einen Index jenseits der Listen-Größe angebe. Wie sich diese Probleme äußern, mag jetzt unterschiedlich sein, aber auf jeden Fall brauche ich Code, der zur Laufzeit damit umgehen kann.
Du kannst jetzt gerne einwenden, daß du den drumherumliegenden Algorithmus so anpassen kannst daß der Fall nicht vorkommt - aber ich kann das genausogut in C++

Außerdem kannst du die falsche Verwendung von Datenypen in C++ genauso unterbinden wie in Haskell (ist nur ein wenig aufwendiger, aber machbar). Die meisten Laufzeitfehler, die mir in letzter Zeit untergekommen sind, basierten auf Rechen- oder Denkfehlern und Daten, die erst zur Laufzeit bekannt sind. Sowas kannst du nicht diagnostizieren indem du es in ein Typ-Korsett presst.

Datentypen beziehen sich auf Werte. In Haskell fällt aber wesentlich mehr in die Klasse Werte als in C++. Funktionen etwa sind auch Werte und haben einen Typen. Kontrollstrukturen (Schleifen, sofern man sie braucht, Exceptions, sogar Labels und Sprünge) sind normale Werte und haben einen Typen. Die gesamte Programmlogik hat einen Typen. Rechenfehler werden nicht abgefangen, aber Denkfehler, die sich auf die Programmlogik beziehen, sehr wohl. Du hast referentielle Transparenz (Entsprechung in C++ wäre etwa: ist f(x) = 3, dann kannst du überall in deinem Programm den Aufruf f(x) durch das Ergebnis 3 ersetzen, ohne dein Programm zu verändern) und kannst durch lazy evaluation viele Algorithmen auf eine Art schreiben, die den Datenfluss expliziter und deshalb weniger fehleranfällig macht. Wie oft hat man ein falsches Ergebnis, weil man Zuweisungen in der falschen Reihenfolge geschrieben hat?

kommt bei mir eher seltener vor.

Daß man Funktionen auch wieder als Werte betrachten kann, ist vielleicht ein Vorteil (wobei C++ auch Funktionszeiger und Funktoren anbietet), daß man Kontrollstrukturen auch als Werte ansehen kann, liegt vermutlich am Konzept der funktionalen Programmierung. Und referenzielle Transparenz habe ich auch noch nicht wirklich benötigt - wenn es mir zu umständlich ist, den Wert von f(x) an mehreren Stellen im Programm ausrechnen zu lassen, packe ich ihn halt in eine Hilfsvariable.

Klar, wenn man die Möglichkeiten einer Sprache einschränkt, kann man innerhalb dieser Möglichkeiten irgendwann alles beweisen. Das Problem ist, daß du mit einer solchen Sprache schneller an die Grenzen dessen kommst, was du darstellen kannst.

Also ich weiß nicht. Ein komplettes HTTP-Framework gibt es bereits in Agda. Dieses Framework demonstriert auch schön, wie man in Agda all die schönen Sachen machen kann, die du willst, und die in Haskell nur sehr aufwendig zu realisieren sind.

Es ist kein Problem, für einen speziellen Anwendungsbereich eine nicht-turingvollständige Sprache zu verwenden, solange es für das reicht, was du damit vorhast. Und zu deinem Glück fallen mir aus dem Stegreif auch nur akademische Beispiele ein, die die Grenzen der Tuing-Vollständigkeit ausnutzen und mit so einer "verkleinerten" Sprache nicht lösbar wären.

Du wolltest doch Fehlerfreiheit durch Typsicherheit ausdrücken (oder war das einer der anderen Haskell-Anhänger - jedenfalls kam von einem von euch die Aussage "wenn es sich compilieren lässt, ist es fehlerfrei"?).

Meine Aussage war, dass ein Programm, das kompiliert, in den meisten Fällen auch funktioniert. Ich schreibe meine Programme so, dass ich nur selten Fehler zur Laufzeit finden muss. Und besonders viel Numerik kommt in meinen Programmen nicht vor, daher habe ich auch selten arithmetische Bugs. Die statisch zu prüfen würde aus einem effizienten 1000-Zeilen-Programm ein sehr ineffizientes, kaum zu überblickendes 100000-Zeilen-Programm machen. Das ist auch der Grund, warum ich dir keine Code-Beispiele gebe. Ich nehme mir nicht ein ganzes Wochenende Zeit, nur um dir zu beweisen, dass es möglich ist, auch solche Beweise zu führen.

Darf man erfahren, was für Programme du so schreibst, bei denen du ohne Arithmetik auskommst? Ich habe beruflich mit Anwendungen zu tun, die einiges zu rechnen, vergleichen und auszuwerten haben, also beschäftige ich mich naturgemäß ein wenig stärker mit dem arithmetischen Aspekt.

volkard schrieb:

ertes schrieb:

Haskell ist typensicher und Programme, die kompilieren, funktionieren meistens auch. Viele Bugs, die in C++ erst zur Laufzeit auftreten würden, fängt in Haskell bereits der Compiler ab. (Eure Interpretation: Ich würde meine Programme nie testen. Ich würde meine Programme so schreiben, dass jede noch so kleine Kleinigkeit statisch garantiert wird.)

Das rührt aus einem Mißverständnis her.
Jeder, der "Effektiv C++ programmieren" gelesen und verstanden hat, macht auch in C++ viele Bugs, die in vielen anderen Sprachen erst zur Laufzeit auftreten würden, zu Compilerfehlern. Wir versuchten zu ergründen, was Haskell da an Mehrwert hat. Und Du bliebst für uns enorm schwammig widersprüchlich leer, weil Du einerseits Codebeispiele gezeigt hast, die dann doch zu extrem waren und Du sie selber nicht verwendest, und andererseits Codebeispiele zeigtest, die verwendbar sind und auch in modernem C++ eine Selbstverständlichkeit sind. Es war kein Mehrwert ersichtlich, obwohl Du dauernd den Mehrwert betont hast. Verwirrend. Also fragt man nach. Und es kommt nur weiter *******.
Wir gingen dummerweise davon aus, daß Du C++ total gut kannst. Weil Du es mehrfach behauptet hast. Ab jetzt spreche ich es auch Dir ab. Es gibt viele mehrjährige C++-Programmierer, die nicht gut sind. Es würde einfach gut erklären, warum Du Dich in Haskell so verknallt hast. Fröhliche Ostern!

Siehe oben. Nur weil du meine Argumente nicht verstehst, brauchst du nicht mit persönlichen Angriffen loslegen. Das ist übrigens gemeinhin ein Hinweis dafür, dass dir selber die Argumente ausgehen.

Die Tatsache, daß du ständig die selben Thesen wiederholst, kann man auch als Hinweis ansehen, daß dir die Argumente ausgehen.