Haskell

GPC

Bashar schrieb:

Ob es Visual Basic Gurus gibt? Das ist doch Perlen vor die Säue.

Klar gibt's auch VB6 Gurus, warum auch nicht. Die werden halt immer weniger, weil es seitens MS keinen Suppport mehr für VB6 gibt und auf .NET die meisten C# anstatt VB.NET nutzen.
VB6 ist halt furchtbar verbose und es fehlen (inzwischen) im Mainstream angekommene Dinge wie Lambdas, Generics/Templates etc, aber es war ja auch als RAD-Tool für GUI bzw. COM ausgelegt und da hat es nicht ohne Grund massive Erfolge gefeiert.

knivil

Gut, dann korrigiere ich mich: Nicht alle koennen auf Korrektheit geprueft werden. Tools wie http://vimeo.com/6687266 habe ich bereits ausprobiert. HLint wird auch konsequent benutzt. Desweiteren ist automatisches Beweisen und Typinferenz eng verbunden: Theorems for free!, d.h. jedes System mit Typinferenz ist schon ein Theorembeweiser.Verifying Haskell Programs Using Constructive Type Theory sieht auch sehr interessant aus.

volkard

Daraus schließe ich, daß es auch kein wesentliches Feature von Haskell ist.

knivil

volkard schrieb:

Daraus schließe ich, daß es auch kein wesentliches Feature von Haskell ist.

Definiere wesentlich!

volkard

knivil schrieb:

Definiere wesentlich!

Na, Du betreibst Haskell nicht, weil Du damit Programme beweisen kannst, sondern weil es hübsch und so elegant ist und einfach Spaß macht.

knivil

Doch, ich moechte mir sicher sein, dass Programme korrekt sind. Dazu reicht mir meist Testen nicht aus bzw. Testen wird unnoetig, wenn ich die Korrektheit beweisen kann. Natuerlich mache ich das nicht fuer jedes Programm/Funktion. Selbstverstaendlich ist das nicht der einzige Grund. Eleganz und Einfachheit spielen auch alle eine Rolle. Diese Eigenschaften haben alle einen gemeinsamen Ursprung: programmierte Mathematik. Zwar bieten andere Sprachen das auch, aber besitzen nicht alle Features von Haskell.

volkard

Ich glaube Dir nicht, daß Du öfters mal Programme oder Funktionen beweist, und deswegen Haskell einsetzt.

Bashar

Warum denn persönlich werden? Es ging doch darum, ob das ein wesentliches Feature von Haskell ist. Es spielt dafür absolut keine Rolle, ob knivil das gerne nutzt.

volkard

Bashar schrieb:

Warum denn persönlich werden? Es ging doch darum, ob das ein wesentliches Feature von Haskell ist. Es spielt dafür absolut keine Rolle, ob knivil das gerne nutzt.

Aber er schrieb:

knivil schrieb:

Doch, ich moechte mir sicher sein, dass Programme korrekt sind. Dazu reicht mir meist Testen nicht aus bzw. Testen wird unnoetig, wenn ich die Korrektheit beweisen kann. Natuerlich mache ich das nicht fuer jedes Programm/Funktion. Selbstverstaendlich ist das nicht der einzige Grund. Eleganz und Einfachheit spielen auch alle eine Rolle. Diese Eigenschaften haben alle einen gemeinsamen Ursprung: programmierte Mathematik. Zwar bieten andere Sprachen das auch, aber besitzen nicht alle Features von Haskell.

Da will er mich veralbern. Das habe ich kurz abgewehrt. Oder veralbert sich selber, ohne es zu bemerken. Ich kann Dir auch den Gefallen tun und es ausführlicher machen:

knivil schrieb:

Doch, ich moechte mir sicher sein, dass Programme korrekt sind.

Ja, das möchten wir alle irgendwie.

knivil schrieb:

Dazu reicht mir meist Testen nicht aus

Dann testest Du schlecht.

knivil schrieb:

bzw. Testen wird unnoetig, wenn ich die Korrektheit beweisen kann.

Hier wird es auffällig. Du testest nicht, weil man die Korrekteheit beweisen KÖNNTE, aber Du beweist auch nicht.
In der Tat bist Du nur sicher, daß es korrekt ist. Mhhm, das schafft man auch in anderen Sprachen. Oh, nicht nur das. Auch in anderen Sprachen kann man Korrektheit beweisen. Tut man ja auch schon eine ganze Weile, erhlich!

knivil schrieb:

Natuerlich mache ich das nicht fuer jedes Programm/Funktion.

Anscheinend für die allerwenigsten, und Du redest um den heißen Brei herum, versuchst, einen anderen Eindruck zu erwecken. Hiergegen wollte ich mich verwehren.

knivil schrieb:

Selbstverstaendlich ist das nicht der einzige Grund. Eleganz und Einfachheit spielen auch alle eine Rolle.

Und natürlich weil es geek ist.
Und der Rätselspaß wie beim Zauberwürfel.

knivil schrieb:

Diese Eigenschaften haben alle einen gemeinsamen Ursprung: programmierte Mathematik.

Alle Programmiersprachen sind programmierte Mathematik. Oder Du hast ein ganz anderes Mathematikverständnis wie ich.

Bashar

volkard schrieb:

Bashar schrieb:

Warum denn persönlich werden? Es ging doch darum, ob das ein wesentliches Feature von Haskell ist. Es spielt dafür absolut keine Rolle, ob knivil das gerne nutzt.

Aber er schrieb:

Ja, auf dein

Na, Du betreibst Haskell nicht, weil Du damit Programme beweisen kannst, sondern weil es hübsch und so elegant ist und einfach Spaß macht.

Dafür gilt mein Einwand natürlich genauso.

knivil schrieb:

Testen wird unnoetig, wenn ich die Korrektheit beweisen kann.

Au weia.

Eisflamme

Wieso? Find ich logisch. Nur Korrektheit beweisen finde ich schwierig.

Bringt einen das denktechnisch weiter, Haskell zu lernen? Ist das ne gute Übung?

Bashar

Tim schrieb:

knivil schrieb:

Testen wird unnoetig, wenn ich die Korrektheit beweisen kann.

Au weia.

Don Knuth schrieb:

Beware of bugs in the above code; I have only proved it correct, not tried it.

@knivil
Soll ich dir nochmal den Diskussionsverlauf schildern (Achtung, rhetorische Frage, ich mache es sowieso)?

audacia: "Ohne grundlegende algebraische Kenntnisse sind viele Konstrukte in Haskell IMO äußerst schwierig zu verstehen. "
Ich: "Welche denn? Monaden etwa? Wie bereits oben geschrieben, kann man von einem Programmierer allerdings auch grundlegende algebraische Kenntnisse erwarten.*"
Du: "Kategorientheorie wird an den seltensten Universitaeten im Fach Informatik gelehrt. Nein, dieses Wissen kann nicht vorausgesetzt werden."

Du gehst also davon aus, dass man Monaden nur verstehen kann, wenn man Kategorientheorie versteht. Mag sein, dass sie daher kommen, aber eigentlich hätte man sie auch selbst "erfinden" können (siehe den von mir vorher verlinkten Artikel). Ich behaupte nicht, dass sie super einfach zu verstehen sind und ich finde es auch unglücklich, dass man gerade "return" gewählt hat um einen Wert in eine Monade zu heben, da das eher verwirrt, aber wenn man sich etwas mit ihnen beschäftigt und nicht immer die do-Notation verwendet, sind sie eigentlich ganz "harmlos".

* hiermit ist nicht die Kategorientheorie gemeint. Diese fällt wohl kaum unter "grundlegende algebraische Kenntnisse".

Bringt einen das denktechnisch weiter, Haskell zu lernen? Ist das ne gute Übung?

Also, ich finde schon. Man löst Probleme einfach in den meisten Fällen ganz anders als in hauptsächlich imperativen Sprachen, häufig auch deutlich eleganter (wobei das natürlich im Auge des Betrachters liegt).
Und Aufgaben mal mit einer etwas anderen Sichtweise lösen schadet sicherlich nicht.

knivil

@volkard: Natuerlich ist es moeglich in imperativen Sprachen die Korrektheit zu beweisen. Es ist aber a) aufwendiger oder b) nur fuer "kleine" Programme durchfuehrbar. Desweiteren legst du mir Worte in den Mund: KOENNTE. Hoer auf damit. Ich meinte: kann!

@Irgendwer:
1.) Monaden Grundlage reicht nicht
2.) Kategorientheorie besteht aus mehr
3.) Haskell besteht aus mehr als nur Kategorientheorie

Du gehst also davon aus, dass man Monaden nur verstehen kann, wenn man Kategorientheorie versteht. Mag sein, dass sie daher kommen, aber eigentlich hätte man sie auch selbst "erfinden" können

Der erste Satz hat nichts mit dem zweiten zu tun. Du bringst Scheinargumente.

Jetzt merkt knivil in seiner Haskell-Verleibtheit nicht mal mehr wie sehr er übertreibt.

@Irgendwer:
1.) Monaden Grundlage reicht nicht
2.) Kategorientheorie besteht aus mehr
3.) Haskell besteht aus mehr als nur Kategorientheorie

Was soll 1) bedeuten?
Was hat 2) damit zu tun?
3) hat so doch auch niemand behauptet. Du warst übrigens derjenige der die Kategorientheorie erst ins Spiel gebracht hat.

Der erste Satz hat nichts mit dem zweiten zu tun.

Was besseres ist dir nicht eingefallen?
Wie stehst du denn zu meiner Aussage im ersten Satz: "Du gehst also davon aus, dass man Monaden nur verstehen kann, wenn man Kategorientheorie versteht."

Sag doch mal klar und deutlich was du meinst, anstatt dir irgendwelche Einzelaussagen herauszugreifen und diese zu kritisieren. Das würde eine Diskussion deutlich einfacher machen...

audacia

Irgendwer schrieb:

Sag doch mal klar und deutlich was du meinst, anstatt dir irgendwelche Einzelaussagen herauszugreifen und diese zu kritisieren. Das würde eine Diskussion deutlich einfacher machen...

Ein anderes Vokabular übrigens auch.

knivil schrieb:

Bullshit! [...]
@volkard: Bullshit! [...]

Warum nicht auch mal Schafkot oder Ziegenmist? Oder Argumente stattdessen?

knivil schrieb:

Bullshit, Haskell hat besseres OOP!

... besser als wer?

Und mal her mit einem Beispiel, an dem man das erkennen kann!

@Irgendwer:
Nun, ich nehme dieses Thema sehr locker, da ich etwa die gleiche Ansicht vertrete wie Paul Graham, aber nicht auf Common Lisp bezogen, sondern auf Haskell. Mir kommt es zugute, dass meine Konkurrenz Haskell nicht kennt oder davon nicht viel hält. Das bringt mir bares Geld, und keiner scheint zu verstehen, wie ich das mache. Das ist gut für mich. In diesem Sinne schneide ich mir eigentlich ins eigene Fleisch, indem ich hier poste, aber ich bin eben nicht so konsequent wie Paul.

Fakt ist: Haskell hat meine Entwicklungszyklen dramatisch verkürzt. Ich mache praktisch kein Debugging mehr, denn sobald meine Programme kompilieren, funktionieren sie auch. Nein, ich meine nicht nur, dass ihre Korrektheit bewiesen ist, sondern dass sie sich auch in der Praxis beweist. Und dabei geht es nicht um irgendwelchen akademischen Kram, sondern um praktische Anwendungen, mit denen ich Geld verdiene (Webseiten hauptsächlich).

Es kommt nicht selten vor, dass ich seitenweise Code schreibe, bevor ich auch nur ein einziges mal kompiliere. Meistens habe ich dann ein bis zwei Typfehler drin (die in C++ zu 99% zu Laufzeitfehlern führen würden). Die behebe ich, und schon funktioniert mein Code. Da können die ganzen C++-Freaks hier noch so wenig von automatischen Beweisverfahren durch Typentheorie halten. Es ist Fakt. Und dadurch kann ich mich auf die eigentliche Aufgabe konzentrieren und Code schreiben, der etwas tut. Das ist vielleicht auch der Grund dafür, dass es keinen anspruchsvollen Debugger für Haskell gibt. Er wird schlicht und ergreifend nicht gebraucht. Und nochmal: Klar werden jetzt jedem C++-Programmierer die Finger jucken, mir zu widersprechen, aber das interessiert mich nicht. Es ist Fakt, und mit diesem Fakt verdiene ich Geld.

Mir wird so oft widersprochen, wenn ich sage, dass Haskell eine geniale Sprache ist. Inzwischen spare ich mir diese Aussage, denn ich kenne die Macht von Haskell und weiß sie zu schätzen, und ich gehöre zu denen, die den direkten Vergleich haben und demnach objektiv beurteilen können. Und wenn man mir nicht glaubt, ist das besser für mich.