Wie können lineare Typen eine solche Implementierung von "Duplikat" verhindern?

Question

Ich habe vor kurzem gelesen the post on Tweag.IO über lineare Typen als ein nützliches Werkzeug zum Ausdrücken von Argumenten nur einmal verwendet (genau). Sie präsentieren das folgende Beispiel:

dup :: a ⊸ (a,a) 
dup x = (x,x) 

Nun, vielleicht habe ich die Idee bin Missverständnis, aber warum konnte das nicht mit umgangen werden:

dup' :: a ⊸ (a,a) 
dup' x = (y,y) 
    where 
    y = x 

Der Artikel erwähnt ausdrücklich Argumente. Gilt das auch für alle Bindungen in der Funktion?

Answer 1

Ich glaube, dieser Artikel gibt fast keine Erklärung der zugrunde liegenden Semantik - nur Beispiele, wie man eine solche Technologie verwendet. Um fair zu sein, ist dies wahrscheinlich ein gutes Format für einen Blogbeitrag.

Sie könnten x ⊸ y als Synonym für 1 x -> y Ansicht, die einen regelmäßigen Pfeil ist, deren Domäne ist 1 x die sagt die Variable a :: 1 x genau einmal verwendet wird. Nach Art der Inferenz erhält y in Ihrem zweiten Beispiel den gefolgerten Typ 1 a, da y = x und x :: 1 a. Dies erstreckt sich auf alle natürlichen Zahlen und die Unendlichkeit. Außerdem kann der reguläre Pfeil x -> y als ω x -> y gelesen werden, wobei ω unendlich ist.

Die paper, die Sie verknüpft haben, gibt die Semantik richtig. Siehe Abschnitt 3.1, Abb. 2 - die Typisierungsregel entsprechend let. Das Standard-Tipp-Urteil x : T wird verallgemeinert zu x :_{q} T (das q sollte ein Index sein). In vorhandenen Haskell-Typ-Semantiken wird ein Begriff mit seinem Typ annotiert. In der vorgeschlagenen Erweiterung des Typsystems wird ein Begriff mit seinem Typ und seiner Multiplizität kommentiert.

Beachten Sie jedoch, dass das let-Konstrukt in diesem Dokument immer eine explizite Typ-Signatur für die Let-gebundene Variable enthält. Mit der Syntax dieses Papiers ist Ihr 2. Programm (und tatsächlich die meisten Haskell-Programme!) Nicht einmal syntaktisch gültig. Aber ich behaupte (ohne Beweis), dass es nicht schwer ist, zu sehen, wie man ein solches Typsystem auf ein System mit mehr Ähnlichkeit mit dem aktuellen Haskell-System verallgemeinern kann. Sehen Sie den Vorschlag für die GHC trac für weitere Details, wie das aussehen könnte.