Haskell
-
Und wenn jetzt alle Haskell anfangen? Säue vor die Perlen?
-
Irgendwer schrieb:
Ohne grundlegende algebraische Kenntnisse sind viele Konstrukte in Haskell IMO äußerst schwierig zu verstehen.
Welche denn? Monaden etwa? Wie bereits oben geschrieben, kann man von einem Programmierer allerdings auch grundlegende algebraische Kenntnisse erwarten.
Das Buch mit dem Ich Haskell programmieren lernen wollte "Introduction to functional progrmaming using Haskell" war das einzige Programmierbuch jemals, in dem sich der Autor genötigt fühlte zu beweisen, dass zwei Ausdrücke das identische Ergebnis bildeten. Nur war der eine Ausdruck 10x schneller, war aber nicht mehr wirklich gut von der Semantik her verständlich. Und der Beweis war auch meiner Erinnerung nach nichttrivial.
Ich weiß nicht, ob eine Sprache so toll ist, in der man bei bestimmten Codeschnipseln den Beweis als Kommentar drüber packen muss.
-
Nur war der eine Ausdruck 10x schneller, war aber nicht mehr wirklich gut von der Semantik her verständlich.
Selbst in C++ ist es häufig der Fall, dass die naive Implementierung nicht die schnellste ist. Schnellere Implementierungen werden dann häufig etwas komplizierter und sollten dann kommentiert werden.
Und der Beweis war auch meiner Erinnerung nach nichttrivial.
Sonst hätte er ihn wohl nicht erklärt, oder?
-
Welche denn? Monaden etwa? Wie bereits oben geschrieben, kann man von einem Programmierer allerdings auch grundlegende algebraische Kenntnisse erwarten.
Kategorientheorie wird an den seltensten Universitaeten im Fach Informatik gelehrt. Nein, dieses Wissen kann nicht vorausgesetzt werden.
Autor genötigt fühlte zu beweisen, dass zwei Ausdrücke das identische Ergebnis bildeten
Nein, es drueckt ein wesentliches Feature von Haskell aus. Korrektheit von Programmen kann bewiesen werden.
-
knivil schrieb:
Autor genötigt fühlte zu beweisen, dass zwei Ausdrücke das identische Ergebnis bildeten
Nein, es drueckt ein wesentliches Feature von Haskell aus. Korrektheit von Programmen kann bewiesen werden.
Echt?
Das wäre supi. Dann könnte ich ja ungelöste mathematische Probleme nach Haskell übersetzen und dort beweisen. Genial! Ich liebe Haskell und den Fanclub.
-
Nein, dieses Wissen kann nicht vorausgesetzt werden.
Man muss die Kategorientheorie nicht verstehen um Monaden schreiben und verwenden zu können. Siehe auch: You could have invented monads
Solche Aussagen wie deine sind es, die dazu führen, dass funktionale Sprachen von den meisten als rein akademische Forschungssprachen verstanden werden.Das wäre supi. Dann könnte ich ja ungelöste mathematische Probleme nach Haskell übersetzen und dort beweisen. Genial! Ich liebe Haskell und den Fanclub.
-
@Irgendwer: Ich kenne die meisten Artikel. Um Monaden zu benutzten, braucht man sie vielleicht nicht verstehen. Aehnliches gilt auch fuer Templates. Ich kann die Container der STL benutzen. Will ich aber Templates darueber hinaus einsetzen, muss ich sie verstehen.
Solche Aussagen wie deine sind es, die dazu führen, dass funktionale Sprachen von den meisten als rein akademische Forschungssprachen verstanden werden.
Bullshit! Der Schritt von Monaden in Haskell auf alle funktionalen Sprachen ist sehr gross.
@volkard: Bullshit! Ich habe nicht von allen Programmen gesprochen.
-
knivil schrieb:
Nein, es drueckt ein wesentliches Feature von Haskell aus. Korrektheit von Programmen kann bewiesen werden.
Lies das nochmal genau durch. So, wie es da steht, sprichst Du von allen Programmen. Und das ist Quatsch.
Manche Programme können auch in anderen Sprachen bewiesen werden. Das ist also nicht der Vorteil. Abgesehen davon, daß die Flieger abtürzen, weil die Spezifikation falsch war, nicht das Programm. Du könntest höchstens herausarbeiten, daß manche Programme in Haskell leichter automatisch bewiesen werden können.
Benutzt Du automatisierte Programmbeweiser?
-
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.
-
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.
-
Daraus schließe ich, daß es auch kein wesentliches Feature von Haskell ist.
-
volkard schrieb:
Daraus schließe ich, daß es auch kein wesentliches Feature von Haskell ist.
Definiere wesentlich!
-
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.
-
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.
-
Ich glaube Dir nicht, daß Du öfters mal Programme oder Funktionen beweist, und deswegen Haskell einsetzt.
-
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.
-
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.
-
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.
-
Wieso? Find ich logisch. Nur Korrektheit beweisen finde ich schwierig.
Bringt einen das denktechnisch weiter, Haskell zu lernen? Ist das ne gute Übung?