Wie ist die Beziehung zwischen statischer Typisierung und faulen funktionalen Sprachen? [geschlossen]

8

Ich bin neugierig auf die Beziehung zwischen statischen Typisierung und faulen funktionalen Sprachen. Ist es zum Beispiel möglich, eine dynamisch faule funktionale Sprache zu haben? Es scheint, als ob alle der faulen funktionalen Sprachen statisch getippt sind (Haskell, Miranda, usw.), und alle dynamischen funktionalen Sprachen verwenden strenge Bewertungen (Clojure, Scheme, etc).

Insbesondere der Wikipedia-Artikel zur Lazy-Bewertung lautet:

  

Bei einer faulen Bewertung ist es jedoch schwierig mit zu kombinieren   zwingende Merkmale wie Ausnahmebehandlung und Eingabe / Ausgabe,   weil die Reihenfolge der Operationen unbestimmt wird. Faule Bewertung   kann Platzlecks einführen.

Welche Rolle spielt die statische Typisierung bei der Vermeidung von Speicherlecks?

    
Josh Voigts 16.10.2012, 01:42
quelle

4 Antworten

14

Ich glaube nicht, dass statische Typen überhaupt eine Rolle spielen. Betrachten wir zum Beispiel die nicht typisierte faule Sprache Lazy Racket . Ich habe keinen Hinweis darauf gehört, dass es Platz in einer Weise verliert, die Haskell (zum Beispiel) nicht hat.

Andererseits sind Nebenwirkungen ein Problem, weil Menschen die Reihenfolge der Auswertung strenger Bewertung als (relativ) natürlich empfinden, und Call-by-Need ist viel schwieriger mental vorherzusagen .

    
Paul Stansifer 16.10.2012, 03:17
quelle
6
  

Welche Rolle spielt die statische Typisierung bei der Vermeidung von Speicherlecks?

Typen können verwendet werden, um die Lebensdauer von Objekten zu verfolgen, wobei statisch das Fehlen von Lecks sichergestellt wird.

Ein Beispiel wären Regionstypen und andere Effekttypen.

    
Don Stewart 16.10.2012 04:52
quelle
3

Faule Auswertung und statische Typisierung sind unabhängige Konzepte.

  1. Untypisiert
  2. Getippt
    • Faule Bewertung Haskell ist ein Beispiel.
    • Eager Bewertung OCaml ist ein Beispiel.

Grob gesagt, Evaluation ist etwas, das passiert, wenn das Programm ausgeführt wird. Das Eingeben geschieht, wenn das Programm kompiliert wird.

Aber natürlich gibt es eine wichtige Entsprechung zwischen einem Typisierungssystem und einer Auswertungsstrategie:

  

Wenn sich ein Term M auf N und reduziert: M: σ ( M ist vom Typ ) σ ) dann N: σ .

Das bedeutet, wenn wir ein Programm ausführen, das einen Typ σ hat, dann den Wert wird den gleichen Typ haben. Ohne diese Eigenschaft ist ein Tippsystem wirklich nutzlos (zumindest für die Programmierung). Dies bedeutet auch, dass wir nach Eingabe von a Programm während der Kompilierung müssen wir uns nicht an die Tippinformationen erinnern wenn wir es auswerten, weil wir wissen, dass das Ergebnis den richtigen Typ haben wird.

Betreffend den Wikipedia-Artikel, den du zitierst. Es gibt zwei verschiedene Dinge:

  1. Imperative Eigenschaften. Dies hängt nicht wirklich mit einem Typisierungssystem zusammen. Das Problem ist, dass, wenn bestimmte Ausdrücke in lazy Einstellungen Nebenwirkungen (wie I / O in den meisten Sprachen) haben, es sehr schwer ist vorherzusagen, wann (wenn überhaupt) ein Nebeneffekt auftritt. Deshalb ist es nach einer faulen Bewertung kaum möglich, eine unreine Sprache zu haben.

    Eine Ausnahme ist die Sprache . Es verwendet ein spezielles Typsystem, um Nebenwirkungen in einer faulen Einstellung zu behandeln. Hier besteht also eine Verbindung zwischen der Evaluierungsstrategie und dem Typisierungssystem durch die Behandlung von Nebenwirkungen: Das Typsystem erlaubt es, Nebenwirkungen so zu behandeln, dass wir eine faule Auswertung behalten können.

  2. Platzlecks. Dies ist ein bekannter Nachteil der Lazy Evaluation. Siehe Nicht bewertete Ausdrücke erstellen oder Kap. 25 Profiling und Optimierung in Real World Haskell. Aber wieder hat das nichts mit Typsystemen zu tun - Sie würden das gleiche Verhalten in einer untypisierten Sprache bekommen.
Petr Pudlák 17.11.2012 11:55
quelle
2

Ich denke, wenn man Dinge von einer allgemeineren Ebene betrachtet, ist es möglich, eine natürliche Beziehung zwischen statischer Typisierung und faulen funktionalen Sprachen zu beobachten. Der Hauptpunkt von statischen Typen besteht darin, die Fähigkeiten des Compilers zu informieren und zu verbessern; Bei der Untersuchung der statisch-dynamischen Unterteilung zwischen Sprachen verfolgt es im Allgemeinen das Schisma zwischen kompiliertem und interpretiertem Code.

Und was ist der Zweck der faulen Bewertung?

Ein berüchtigter, retrospektiver Artikel von Peyton-Jones et al. beschreibt eine faule Bewertung als "das Haarhemd", das die Sprache rein funktional hält. Seine Metapher vermittelt den tief verwurzelten Idealismus der Denotationssemantik der Haskell-Gemeinschaft. Der grundlegende Vorteil einer nicht-strikten Evaluierung besteht darin, dass sie die Möglichkeiten zur Strukturierung von Code auf eine Weise transformiert, die dieses Denotationsparadigma ermöglicht. In der berüchtigten faulen Evaluierungsdebatte von Bob Harper und der Haskell-Gemeinschaft zeigt Prof. Harper die Herausforderungen, die faule Evaluationen für praktische Programme bedeuten - und unter Lennart Augustsssons Faulheitsverteidigung illustriert dieser am besten den Punkt:

  

"Ich habe meine größte Beschwerde der strengen Bewertung für den letzten gespeichert. Strenge Bewertung ist grundlegend fehlerhaft für die Wiederverwendung von Funktionen. [...] Mit strenger Auswertung können Sie nicht mehr mit einem direkten Gesicht sagen Menschen: keine Rekursion verwenden , wiederhole die Rekursionsmuster in map, filter, foldr, etc. Es funktioniert einfach nicht (im Allgemeinen). [...] strikte Evaluation hält dich wirklich davon ab, Funktionen wiederzuverwenden, so wie du es mit Faulheit tun kannst. "

Und für sein Beispiel der Wiederverwendung von Funktionen durch Lazy Evaluation bietet Augustsson an: "Es ist ganz natürlich, die Funktion any durch die Wiederverwendung der Funktionen map und or auszudrücken. " So faul Die Bewertung ergibt sich aus diesem Bild als ein ziemlich kostspieliges Sprachmerkmal, das im Dienste eines natürlicheren Kodierungsstils verwendet wird.

Was brauchen wir noch, um einen abstrakten, denotationalen Codierungsstil aufrechtzuerhalten? Ein leistungsfähiger optimierender Compiler könnte sich als nützlich erweisen! Selbst wenn es keine technische oder notwendige Verbindung zwischen statischen Typen und fauler Auswertung gibt, sind die beiden Merkmale auf dasselbe Ziel ausgerichtet. Es ist nicht so überraschend, dass sie oft zusammen erscheinen.

    
sacheie 17.11.2012 02:28
quelle