Haskell



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

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

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

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

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

    Hier die gut spezifizierte Variante und interessanterweise sogar flexiblere Variante:

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

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

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

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

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

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

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

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

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

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

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

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

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



  • ertes schrieb:

    ...

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



  • ertes schrieb:

    Und schließlich zum Abschluss: Hier geben viele Leute sehr unqualifizierten Müll über Haskell ab

    Ich sehe es durch die Postings der Haskell-Jünger als bewiesen an, daß die Glorifizierung dieser Sprache völlig verfehlt ist. Die fantastischen Vorteile sind gar nicht so fantastisch und die Haskell-Programmierer vergleichen sich mit Programmieranfängern in anderen Sprachen.

    Vorteile: Automatische Parallelisierung, die dafür sorgen kann, die Grundlangsamkeit überwinden.
    Vorteil: Man kann Code bauen, der viele Dummheitsfehler zu Compilerfehlern macht, aber das kann man in vielen Sprachen, und das garantiert noch keine Korrektheit und macht wenn man's übertreibt, mehr Arbeit, als einfach richtig zu programmieren.
    Vorteil: Man kann jetzt in Haskell besser pr0ggern als damals in C++, wen wundert's? Möchte wissen, wieviel besser man erst pr0ggern könnte, wenn man nach C# gewechselt wäre.



  • ertes schrieb:

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

    Und wie unterscheidet sich der Typ der Identitätsfunktion von jeder anderen Umwandlungsfunktion in einem Typ (Nachfolger, Inversion, ...)?

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

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

    Hier die gut spezifizierte Variante und interessanterweise sogar flexiblere Variante:

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

    ...

    Ich gehe jetzt mal nicht komplett ins Detail, aber mit C++ kann ich genauso strenge Typprüfungen zulassen, indem ich die meine Klassen und Funktionen entsprechend restriktiv auslege.
    Und solange du mir nicht zeigst, wie die Umsetzung dieser Funktionen aussehen würde, beweist dein Beispiel gar nichts.

    Edit: Und sobald du mit Eingabedaten umgehen mußt, die von außerhalb deines Programms stammen können, nützen dir die vom Compiler gelieferten Typ-Validierungen gar nichts mehr.

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

    Sowiet ich die Diskussion bisher verfolgen konnte, was "das mit der Korrektheit" eines der Hauptargumente der Haskell-Befürworderer hier.

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

    Ich kann durchaus akzeptieren, daß C++ nicht unfehlbar ist. Aber du scheinst das von Haskell zu glauben.

    Was die Mächtigkeit einer Sprache angeht, solltest du dich mal mit den Grundlagen der Berechenbarkeitstheorie beschäftigen.

    @knivil: Dann versuch dich mal an einem interaktiven System: Der Nutzer bekommt eine Sammlung von Datensätzen, kann davon einzelne suchen, bearbeiten und ändern. (z.B. ein Telefonbuch)



  • @volkard: Du bestätigst meine Aussage. Du gibst ebenso nur unqualifizierten Müll ab, und du kannst nicht mal das Gegenteil rechtfertigen, oder willst du mir sagen, dass du Haskell mal ernsthaft unter die Lupe genommen und verwendet (!) hast, statt nur darüber zu lesen? Alle Punkte deines ersten Absatzes kann ich 1:1 zurückwerfen, indem ich "Haskell" und "C++" in deinem Beitrag vertausche. Ja, auch deinen inhaltlosen Spruch über "Haskell-Jünger". Unterschied zwischen uns beiden: Ich hätte Recht. Ich kenne beide Sprachen. Du nicht.

    Zu deinem zweiten Absatz:
    Vorteil 1: Hast du nur irgendwelche Benchmarks von 2005 oder auf Drogen geschriebene Blogs gelesen oder woher hast du den Blödsinn? Wenn du dir mal das Language-Shootout anschaust, wirst du feststellen, dass Haskell sich im selben Performance-Level bewegt wie C++. Oftmals ist es 20% langsamer, aber es ist auch gerne mal schneller. Außerdem hat mein Programm schon lange fertiggerechnet, während du noch dein C++-Programm schreibst. Die Parallelisierung als Kompensierung für schlechte Performance hinzustellen zeigt, dass dir die Argumente ausgehen, und belegen kannst du dein Geschwafel auch nicht.

    Vorteil 2: Auf den Quatsch gehe ich erst gar nicht ein, da du Haskell nicht verstehst. Wenn ich mich irre, magst du deine Aussage vielleicht mit einem Beispiel untermauern und nicht nur irgendwelche Sprüche in den Raum werfen? Schon witzig, dass hier so viele negative Aussagen über Haskell gemacht werden, aber keine davon wird mit aktuellen (!) Referenzen oder Beispielen belegt.

    Vorteil 3: Ist dir eigentlich bewusst, dass C++0x/C++1x (oder wie auch immer es jetzt heißt) und C# viele Konzepte beinahe 1:1 von Haskell kopiert haben? Das Spiel geht noch weiter: F# hat das komplette Monadenkonzept in schwächerer Variante von Haskell übernommen, sogar inklusive einer abgeänderten Form der Syntax. Haskell ist also so schlecht, dass alle anderen Sprachen die Features übernehmen. Sogar die allgemeine Sprachsyntax, die ursprünglich von OCaml kommt, wurde in neueren Versionen an Haskell angelehnt. Und im Falle von C++ werden Sprachfeatures übernommen, speziell um die Schwächen vom C++-Standard auszumerzen. Informiere dich erst mal, bevor du dein Gebrabbel abgibst. 😉

    Falls du es noch nicht gemerkt hast: Ich interessiere mich allgemein für Programmiersprachen und nehme die Dinge genau unter die Lupe, bevor ich urteile. Also komm mir nicht mit deiner einseitigen C++-Scheuklappen-Ansicht.

    CStoll schrieb:

    Und wie unterscheidet sich der Typ der Identitätsfunktion von jeder anderen Umwandlungsfunktion in einem Typ (Nachfolger, Inversion, ...)?

    Ich verstehe die Frage nicht, aber es gibt in Haskell genau drei Funktionen des Typs a → a. Die erste ist die Identitätsfunktion, die zweite geht mit ihrem Parameter in eine Endlosschleife (sie divergiert), die dritte ist selbst eine Endlosschleife. Unterschied zwischen den letzten beiden: Im ersteren Fall ist f noch definit und kann an eine strikte Funktion übergeben werden, ohne dass diese divergiert, f x nicht. Im letzteren Fall ist bereits f indefinit und führt eine strikte Funktion zur Divergenz. Du kannst keine andere Funktion schreiben, die diesen Typ besitzt.

    Beim Ableiten ist die Frage: Welche vollständig definite (also nirgends divergierende) Funktion erfüllt diesen Typ? Mit anderen Worten: Welche Funktion, die niemals in eine Endlosschleife geht, nie eine Exception wirft, also generell immer zu einem Ergebnis konvergiert, erfüllt den angegebenen Typ? Ein abgeleitetes Programm terminiert also immer oder nutzt Korekursion, um mit der realen Welt zu kommunizieren (wenn man es wirklich so weit treiben will – ich nicht).

    Ich gehe jetzt mal nicht komplett ins Detail, aber mit C++ kann ich genauso strenge Typprüfungen zulassen, indem ich die meine Klassen und Funktionen entsprechend restriktiv auslege.
    Und solange du mir nicht zeigst, wie die Umsetzung dieser Funktionen aussehen würde, beweist dein Beispiel gar nichts.

    In Haskell musst du den Compiler umschreiben, um die Spezifikation zu brechen, in C++ nicht. Und in Haskell sind die Typen von Grund auf strikter, also schon in der base-Bibliothek. Das sind die Unterschiede, aber egal, lassen wir das Thema. Wie gesagt: Für mich ist das nur ein zusätzlicher Vorteil von Haskell, aber nicht der Hauptvorteil.

    Für ein praktisches Beispiel kannst du dir gerne einige der Bibliotheken ansehen, die ich veröffentlicht habe. Drei Beispiele sind ismtp, ihttp und dnscache. Diese habe ich im produktiven Einsatz.

    Sowiet ich die Diskussion bisher verfolgen konnte, was "das mit der Korrektheit" eines der Hauptargumente der Haskell-Befürworderer hier.

    Mag sein, aber nicht meins.

    Ich kann durchaus akzeptieren, daß C++ nicht unfehlbar ist. Aber du scheinst das von Haskell zu glauben.

    Was die Mächtigkeit einer Sprache angeht, solltest du dich mal mit den Grundlagen der Berechenbarkeitstheorie beschäftigen.

    Nein, ich glaube nicht, dass Haskell unfehlbar ist. Da gibt es bessere Sprachen, und ich habe auch welche genannt. Wenn es mir um Unfehlbarkeit ginge, würde ich in Agda programmieren, nicht in Haskell. Mir geht es aber eher um Produktivität. Mit den Grundlagen der Berechenbarkeitstheorie bin ich durchaus vertraut. Aber Mächtigkeit einer Programmiersprache basiert auf etwas anderem. Sonst müsste man schließen, dass es keinen Unterschied macht, ob man in C++ oder Assembler programmiert.

    @knivil: Dann versuch dich mal an einem interaktiven System: Der Nutzer bekommt eine Sammlung von Datensätzen, kann davon einzelne suchen, bearbeiten und ändern. (z.B. ein Telefonbuch)

    Ja, das ist eine sehr gute Anwendung. Mach eine Kommandozeilenversion daraus. Wenn diese funktioniert, ist es relativ leicht, daraus eine konkurrente Netzwerkversion zu machen, z.B. mit Sockets und STM. Hier zeigt Haskell auch seine wahren Stärken.



  • ertes schrieb:

    CStoll schrieb:

    Und wie unterscheidet sich der Typ der Identitätsfunktion von jeder anderen Umwandlungsfunktion in einem Typ (Nachfolger, Inversion, ...)?

    Ich verstehe die Frage nicht, aber es gibt in Haskell genau drei Funktionen des Typs a → a. Die erste ist die Identitätsfunktion, die zweite geht mit ihrem Parameter in eine Endlosschleife (sie divergiert), die dritte ist selbst eine Endlosschleife. Unterschied zwischen den letzten beiden: Im ersteren Fall ist f noch definit und kann an eine strikte Funktion übergeben werden, ohne dass diese divergiert, f x nicht. Im letzteren Fall ist bereits f indefinit und führt eine strikte Funktion zur Divergenz. Du kannst keine andere Funktion schreiben, die diesen Typ besitzt.

    OK, ich formuliere meine Frage neu: Wie würdest du in Haskell den Typ einer Nachfolger-Funktion oder der Negativ-Funktion (f(x)=-x) beschreiben?
    Und nur zur Sicherheit: Was verstehst du unter dem Typ einer Funktion? Ich verstehe daunter die Angabe, welche Argument- und Ergebnistypen dieser Funktion (bzw. ihr Definitions- und Wertebereich).



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

    Noe, wir sind aus dem Land C++ nach Haskell-Heaven gegangen und berichten euch von unseren Erfahrungen. Es hat mich auch zu einem besseren C++ Programmierer gemacht. Natuerlich ist Ablehnung vorprogrammiert, wie z.B. volkard deutlich zeigt. Die Basis dieser Haltung ist aber eher religioeser Natur als wirklich fundiert. Schade ...

    Ich verstehe die Frage nicht, aber es gibt in Haskell genau drei Funktionen des Typs a → a.

    Es gibt genau eine, die fuer alle Typen sinnvoll ist, nicht nur im Kontext von Zahlen oder Listen. Betont man das nicht, fuehrt es oft zu Missverstaendnissen. Hier: http://www.youtube.com/watch?v=h0OkptwfX4g . Die Funktion f(x) = -x hat den Typ f :: (Num a) => a -> a . Sie macht also nur Sinn fuer Typen, die Instanzen von Num sind. Und bevor Fragen kommen: http://en.wikipedia.org/wiki/Type_class , aehnelt den Interfaces beispielsweise in Java.

    @knivil: Dann versuch dich mal an einem interaktiven System: Der Nutzer bekommt eine Sammlung von Datensätzen, kann davon einzelne suchen, bearbeiten und ändern. (z.B. ein Telefonbuch)

    Eine Liste von Haskellanwendungen findest du sicher im Web. Beispielsweise ist das Spiel DefCon von Introversion Software mit Haskell programmiert. Andere setzen Haskell im embedded Bereich ein.



  • CStoll schrieb:

    OK, ich formuliere meine Frage neu: Wie würdest du in Haskell den Typ einer Nachfolger-Funktion oder der Negativ-Funktion (f(x)=-x) beschreiben?

    Kommt darauf an, was du beweisen willst. Ohne Beweise sind die Typen ziemlich simpel:

    negate :: Num aaa
    succ :: Num aaa

    Das sind auch die Typen, die man in der base-Bibliothek findet. Wenn du hingegen Beweisführung haben willst, gibt es zwei Varianten. Beispiel: Du willst eine Funktion schreiben, die eine nichtnegative Zahl entgegennimmt. Der Typ könnte so aussehen:

    sqrt :: PosInt → PosInt

    Mit diesem Typ müsstest du allerdings zwei Negierungsfunktionen schreiben, was ja nicht Sinn der Sache ist. Eine wirklich sichere Alternative verwendet einen sog. Phantom-Typen:

    data NegSign
    data NonnegSign
    data FlippedSign s

    data SInt s where
     SZero :: SInt NonnegSign
     SSucc :: SInt NonnegSign → SInt NonnegSign
     SNegate :: SInt s → SInt (FlippedSign s)

    class HasSign a where
     type SignOf a

    instance HasSign (SInt NonnegSign) where
     type SignOf (SInt NonnegSign) = NonnegSign

    instance HasSign (SInt NegSign) where
     type SignOf (SInt NegSign) = NegSign

    instance HasSign (SInt (FlippedSign NonnegSign)) where
     type SignOf (SInt (FlippedSign NonnegSign)) = NegSign

    instance HasSign (SInt (FlippedSign (FlippedSign s))) where
     type SignOf (SInt (FlippedSign (FlippedSign s))) = SignOf s

    sqrt :: (HasSign a, SignOf a ~ NonnegSign) ⇒ aa

    Wie du siehst, ist das schon sehr viel Tipparbeit, um statisch zu garantieren, dass sqrt nur nichtnegative Zahlen erhält. Abgesehen davon ist die Zahlendarstellung, die ich oben gewählt habe, sehr ineffizient. Daran ließe sich etwas machen, aber dann wäre der Code noch länger. Haskell ist für diese Art von Beweisführung nicht geeignet. Es ist möglich, aber ziemlich aufwendig. Deswegen wird Haskell im Allgemeinen als Programmiersprache und nicht als Beweisassistent bezeichnet. Agda und Coq hingegen sind richtige Beweisassistenten. Mit denen lässt sich so etwas wesentlich leichter ausdrücken, da es in diesen Sprachen keine scharfe Linie mehr zwischen Typ und Wert gibt.

    Die Sache mit den Phantomtypen kann allerdings sehr nützlich sein, um etwa zu beweisen, dass Resourcen nur dort verwendet werden, wo sie auch Sinn ergeben. Du kannst beispielsweise garantieren, dass ein Datei-Handle nach dem dazugehören hClose nicht mehr verwendet werden kann, und zwar statisch. Wie das geht, steht in einem meiner früheren Beispiele.

    Ein Phantomtyp ist übrigens einfach nur ein Parameter eines Typs, der nicht verwendet wird. Er dient nur zu Zwecken von statischen Garantien.

    Und nur zur Sicherheit: Was verstehst du unter dem Typ einer Funktion? Ich verstehe daunter die Angabe, welche Argument- und Ergebnistypen dieser Funktion (bzw. ihr Definitions- und Wertebereich).

    So ist es. Allerdings sind Funktionen in Haskell normale Werte und der Typkonstruktor für Funktionen (→) unterscheidet sich nicht von anderen Typkonstruktoren. Damit gibt Haskell jegliche Sonderstellung von Funktionen auf.



  • knivil schrieb:

    Noe, wir sind aus dem Land C++ nach Haskell-Heaven gegangen und berichten euch von unseren Erfahrungen. Es hat mich auch zu einem besseren C++ Programmierer gemacht. Natuerlich ist Ablehnung vorprogrammiert, wie z.B. volkard deutlich zeigt. Die Basis dieser Haltung ist aber eher religioeser Natur als wirklich fundiert. Schade ...

    Ich hab mal versucht mit Haskell ein einfaches Anfängerprogramm zu schreiben und fand es ziemlich unschön, was ich hinbekommen hab. Kannst du (oder sonst wer) das Programm von unten mal in Haskell schreiben, um zu zeigen, dass es schön geht.

    #include <string>
    #include <iostream>
    #include <ctime>
    
    int main()
    {
    	int maxNr = 12;
        srand(time(0));
    	int geld = 100;
    	bool ende = false;
    	while ( !ende ) {
    		int setzen = 0;
    		do {
    			std::cout << "\nSie haben " << geld << " Geld. Wieviel wollen Sie setzen? ";
    			std::cin >> setzen;
    		} while (setzen <= 0 || setzen > geld );
    
    		int zahl = 0;
    		std::cout << "Auf welche Zahl wollen Sie setzen (1-" << maxNr << ")? ";
    		std::cin >> zahl;
    
    		int wurf = 1 + rand() % maxNr;
    		std::cout << wurf << " wurde geworfen.\n";
    		if ( wurf == zahl ) {
    			geld += setzen * 10;
    		}
    		else {
    			geld -= setzen;
    		}
    
    		if ( geld > 0 )	{
    			std::string weiter;
    			std::cout << "Sie haben " << geld << " Geld. Wollen Sie weiterspielen (j/n)? ";
    			std::cin >> weiter;
    			ende = weiter == "n";
    		}
    		else {
    			ende = true;
    		}
    	}
    	std::cout << "\nSie haben " << geld << " Geld. Gratulation! ;-)\n";
        return 0;
    }
    


  • Dieses Beispiel ist in diesem Thread nicht neu. Aber ich gebe naechste Woche meine Diplomarbeit ab. Wird wohl davor nix. Um die Wartezeit zu verkuerzen, kannst du dir gern http://blog.willdonnelly.net/2009/10/14/brians-purely-functional-brain/ ansehen. Dort hast du Zufall, Grafik und Multithreading. Vielleicht willst du das ja mal in C Programmieren?



  • @ertes, volle Zustimmung von mir!

    Aber wer noch nie mit funktionalen Programmiersprachen gearbeitet hat, dem kann man schwer diese Denkweise vermitteln.
    Schade, daß ich jetzt nicht mehr hier den Sourcecode für meine Diplomarbeit habe (u.a. Programmierung eines kompletten Parsers sowie Verfahren zur Pattern-Matching auf langen (Gen)-Sequenzen in Gofer, einer anderen (älteren) funktionalen Sprache).

    Auch das Spiel 'Mastermind' hatte ich damals innerhalb von einem halben Tag in Gofer programmiert.

    Aber besonders beeindruckend fand ich damals die kurze Def. des QuickSort-Algos:

    qs [] = []
    qs (x:xs) = qs [y|y<-xs; y<=x] ++ [x] ++ qs [y|y<-xs; y>x]
    

    (ich hoffe, ich habe jetzt hier keinen Tippfehler drin 😉



  • Hab ich mir als Anfängerprogramm zufällig das am schwersten zu programmierende Haskell Programm der Welt ausgesucht oder warum kann hier keiner das in 5 Minuten in Haskel kurz schreiben?



  • knivil schrieb:

    Noe, wir sind aus dem Land C++ nach Haskell-Heaven gegangen und berichten euch von unseren Erfahrungen. Es hat mich auch zu einem besseren C++ Programmierer gemacht.

    Warst du nicht derjenige, der behauptete, Exceptions wären Teufelszeug und richtige C++-Programmierer würden Fehlercodes benutzen? Ich erinnere mich da an so einen seitenlangen Thread mit Shade Of Mine als Antipoden...

    knivil schrieb:

    Natuerlich ist Ablehnung vorprogrammiert, wie z.B. volkard deutlich zeigt.

    Das ist eine petitio principii. Du /willst/ diese Reaktion, wie deine Wortwahl deutlich zeigt.

    knivil schrieb:

    Die Basis dieser Haltung ist aber eher religioeser Natur als wirklich fundiert.

    Ich glaube, es war ertes, der den religiösen Aspekt von Haskell ins Spiel brachte.

    knivil schrieb:

    Dieses Beispiel ist in diesem Thread nicht neu. Aber ich gebe naechste Woche meine Diplomarbeit ab. Wird wohl davor nix.

    Wohlgemerkt hätte ein halbwegs erfahrener Benutzer jeder beliebigen handelsüblichen Hochsprache dieses Programm in etwa zehn Minuten schreiben können 😉



  • Ich erkenne die Unwahrheit, wenn sie zu schreien beginnt.
    http://grander.com/en/products
    http://www.nucleostop.de/
    http://www.aquapol-sachsen.de/index.php?go=product/advantage
    Ihr seid nicht mehr über diesem Niveau, sorry. Es kann keiner von mir verlangen, sich da noch tief einzuarbeiten. Es ist höchst interessant, daß Akkupunktur, Grandnerwasser und Aquapol bei manchen Leuten funktionieren. Aber bei mir definitiv nicht, weil ich nicht an solchen Hokuspokus glaube. Wenn Du persönlich davon begeistert bist, und es Dir geholfen hat, dann bitte. Aber gegen den religiösen Feldzug stehe ich hier und widerspreche.



  • Ich glaube, es war ertes, der den religiösen Aspekt von Haskell ins Spiel brachte.

    Ich glaube jeder hat seinen Teil dazu beigetragen.

    Wohlgemerkt hätte ein halbwegs erfahrener Benutzer jeder beliebigen handelsüblichen Hochsprache dieses Programm in etwa zehn Minuten schreiben können

    Magst du eine Version in Scheme? Ich bin nicht hier um irgendwen zu ueberzeugen, auch wenn es den Anschein hat. Die Muehe von ertes wuerde ich mir nicht machen.

    Warst du nicht derjenige, der behauptete, Exceptions wären Teufelszeug und richtige C++-Programmierer würden Fehlercodes benutzen? Ich erinnere mich da an so einen seitenlangen Thread mit Shade Of Mine als Antipoden...

    Das hat nur bedingt was mit dem Thema zu tun. In Haskell habe ich wenig ueber Exceptions gelernt. Du kannst gern den entsprechenden Thread verlinken, damit ich selbst nachsehen kann. No review, no study.

    Das ist eine petitio principii. Du /willst/ diese Reaktion, wie deine Wortwahl deutlich zeigt.

    Nur kam diese Reaktion vor dem was du zitierst. Ich kann diese Logik nicht ganz nachvollziehen. Wie kann ich etwas erbitten, was schon lange eingetreten ist?

    Und nu geht es mal wieder nicht mehr um das Thema Haskell ... kein Wunder das der Thread bereits so lang ist.



  • ertes schrieb:

    CStoll schrieb:

    OK, ich formuliere meine Frage neu: Wie würdest du in Haskell den Typ einer Nachfolger-Funktion oder der Negativ-Funktion (f(x)=-x) beschreiben?

    Kommt darauf an, was du beweisen willst. Ohne Beweise sind die Typen ziemlich simpel:

    negate :: Num aaa
    succ :: Num aaa

    Das sind auch die Typen, die man in der base-Bibliothek findet. Wenn du hingegen Beweisführung haben willst, gibt es zwei Varianten. Beispiel: Du willst eine Funktion schreiben, die eine nichtnegative Zahl entgegennimmt. Der Typ könnte so aussehen:

    sqrt :: PosInt → PosInt

    Und was hindert mich nun daran, die succ-Funktion an einer Stelle einzusetzen, an der in meinem Konzept/Spezifikation eigentlich die negate-Funktion erwartet würde?

    Eine wirklich sichere Alternative verwendet einen sog. Phantom-Typen:

    data NegSign
    data NonnegSign
    data FlippedSign s

    data SInt s where
     SZero :: SInt NonnegSign
     SSucc :: SInt NonnegSign → SInt NonnegSign
     SNegate :: SInt s → SInt (FlippedSign s)

    class HasSign a where
     type SignOf a

    instance HasSign (SInt NonnegSign) where
     type SignOf (SInt NonnegSign) = NonnegSign

    instance HasSign (SInt NegSign) where
     type SignOf (SInt NegSign) = NegSign

    instance HasSign (SInt (FlippedSign NonnegSign)) where
     type SignOf (SInt (FlippedSign NonnegSign)) = NegSign

    instance HasSign (SInt (FlippedSign (FlippedSign s))) where
     type SignOf (SInt (FlippedSign (FlippedSign s))) = SignOf s

    sqrt :: (HasSign a, SignOf a ~ NonnegSign) ⇒ aa

    Wie du siehst, ist das schon sehr viel Tipparbeit, um statisch zu garantieren, dass sqrt nur nichtnegative Zahlen erhält. Abgesehen davon ist die Zahlendarstellung, die ich oben gewählt habe, sehr ineffizient. Daran ließe sich etwas machen, aber dann wäre der Code noch länger. Haskell ist für diese Art von Beweisführung nicht geeignet. Es ist möglich, aber ziemlich aufwendig. Deswegen wird Haskell im Allgemeinen als Programmiersprache und nicht als Beweisassistent bezeichnet. Agda und Coq hingegen sind richtige Beweisassistenten. Mit denen lässt sich so etwas wesentlich leichter ausdrücken, da es in diesen Sprachen keine scharfe Linie mehr zwischen Typ und Wert gibt.

    Und jetzt mußt du mir nur noch demonstrieren, wie du eine nackte Zahl (von der du zur Compilierzeit nur weißt, daß sie existiert) in dieses HasSign-Konstrukt verpacken willst.

    Und nur zur Sicherheit: Was verstehst du unter dem Typ einer Funktion? Ich verstehe daunter die Angabe, welche Argument- und Ergebnistypen dieser Funktion (bzw. ihr Definitions- und Wertebereich).

    So ist es. Allerdings sind Funktionen in Haskell normale Werte und der Typkonstruktor für Funktionen (→) unterscheidet sich nicht von anderen Typkonstruktoren. Damit gibt Haskell jegliche Sonderstellung von Funktionen auf.

    Das habe ich auch nicht bestritten.

    PS: Das Typsystem ist jetzt klarer - und anscheinend liegen die Typ-Definitionen näher an C#-Generics (man muß explizit angeben, was man von den beteiligten Typen erwartet) als an einem C++ Template (die benötigten Operationen ergeben sich aus der Funktionsdefinition). Das erhöht wirklich die Sicherheit der verwendeten Typen, beschränkt aber imho die Flexibilität.



  • knivil schrieb:

    Noe, wir sind aus dem Land C++ nach Haskell-Heaven gegangen und berichten euch von unseren Erfahrungen.

    Auf diesem Neveau wäre alles ok.

    knivil schrieb:

    Es hat mich auch zu einem besseren C++ Programmierer gemacht.

    Auch ok. Lisp hat mich auch zu einem besseren C++-Programmierer gemacht. Ich empfehle sogar jedem, der in C++ weiterkommen will, einen Ausflug in eine Sprache zu machen, die funktionale Programmierung stark fordert. Und ohne Forth hätte ich nie das Programm zum greorianischen Kalender in Brainfuck hingekriegt.



  • knivil schrieb:

    Du kannst gern den entsprechenden Thread verlinken, damit ich selbst nachsehen kann. No review, no study.

    Ich glaube kaum, daß du dich an diese 16 Seiten nicht erinnern kannst 😉
    http://www.c-plusplus.net/forum/235778

    knivil schrieb:

    Das ist eine petitio principii. Du /willst/ diese Reaktion, wie deine Wortwahl deutlich zeigt.

    Nur kam diese Reaktion vor dem was du zitierst.

    Pars pro toto.



  • audacia schrieb:

    knivil schrieb:

    Du kannst gern den entsprechenden Thread verlinken, damit ich selbst nachsehen kann. No review, no study.

    Ich glaube kaum, daß du dich an diese 16 Seiten nicht erinnern kannst 😉
    http://www.c-plusplus.net/forum/235778

    Abgesehen dass der Thread die Halbwertzeit erreicht hat.



  • audacia schrieb:

    Ich glaube kaum, daß du dich an diese 16 Seiten nicht erinnern kannst 😉
    http://www.c-plusplus.net/forum/235778

    Der erklärt jedenfalls wunderbar, warum knivil jetzt in Haskell so ungemein viel besser programmiert als er es damals in C++ getan hat. Das hatte ich schon aus seinen Postings geschlossen. Hübsch, es nochmal so deutlich lesen zu dürfen.


Anmelden zum Antworten