Scala-Constraint-basierte Typen und Literale

Question

Ich überlegte, ob es in Scala möglich wäre, einen Typ wie NegativeNumber zu definieren. Diese Art würde eine negative Zahl darstellen und es würde durch den Compiler ähnlich wie Ints, Streicher usw.

val x: NegativeNumber = -34 
val y: NegativeNumber = 34 // should not compile 

Ebenfalls geprüft werden:

val s: ContainsHello = "hello world" 
val s: ContainsHello = "foo bar" // this should not compile either 

ich diese Typen verwenden könnten wie andere Arten, zum Beispiel:

def myFunc(x: ContainsHello): Unit = println(s"$x contains hello") 

Diese eingeschränkten Typen können durch zufällige Typen (Int, String) unterstützt werden.

Ist es möglich, diese Typen (vielleicht mit Makros) zu implementieren?

Wie wäre es mit benutzerdefinierten Literalen?

val neg = -34n //neg is of type NegativeNumber because of the suffix 
val pos = 34n // compile error 

Answer 1

Leider ist dies nicht etwas, das Sie leicht zur Kompilierzeit überprüfen könnten. Nun - zumindest nicht, wenn Sie die Operationen auf Ihrem Typ nicht einschränken. Wenn Sie lediglich überprüfen möchten, ob ein Zahlenliteral ungleich Null ist, können Sie problemlos ein Makro schreiben, das diese Eigenschaft überprüft. Ich sehe jedoch keinen Nutzen darin, zu beweisen, dass ein negatives Literal tatsächlich negativ ist.

Das Problem ist nicht eine Einschränkung von Scala - die ein sehr starkes Typsystem hat - sondern die Tatsache, dass Sie (in einem einigermaßen komplexen Programm) nicht jeden möglichen Zustand statisch kennen können. Sie können jedoch versuchen, die Menge aller möglichen Zustände zu übertreffen.

Betrachten wir das Beispiel der Einführung eines Typs NegativeNumber, der immer nur eine negative Zahl darstellt. Der Einfachheit halber definieren wir nur eine Operation: plus.

Nehmen wir an, Sie würden nur die Addition von mehreren NegativeNumber erlauben, dann könnte das Typsystem verwendet werden, um zu garantieren, dass jede NegativeNumber tatsächlich eine negative Zahl ist. Dies scheint jedoch sehr restriktiv zu sein, so dass ein nützliches Beispiel es uns sicherlich erlauben würde, mindestens einen NegativeNumber und einen allgemeinen Int hinzuzufügen.

Was ist, wenn Sie einen Ausdruck haben val z: NegativeNumber = plus(x, y) wo Sie nicht wissen, den Wert von x und y statisch (vielleicht hat sie von einer Funktion zurückgegeben werden). Woher weißt du (statisch), dass z eine negative Zahl ist?

Ein Ansatz, das Problem zu lösen wären Abstract Interpretation einzuführen, die auf einer Darstellung des Programms (Source Code, Abstract Syntax-Baum, ...) ausgeführt werden muss.

Zum Beispiel könnten Sie definieren einen Lattice auf die Zahlen mit den folgenden Elementen:

• Top: alle Zahlen
• +: alle positiven Zahlen
• 0: Die Zahl 0
• -: alle negativen Zahlen
• Bottom: keine Zahl - nur eingeführt, dass jedes Paar von Elementen hat eine untere Grenze

mit der Bestellung Top> (+, 0, -)>Bottom.

Dann müssen Sie Semantik für Ihren Betrieb definieren. Unter der kommutativen Methode plus aus unserem Beispiel:

• plus(Bottom, something) ist immer Bottom, da Sie nicht etwas mit ungültigen Zahlen
• plus(Top, x), x != Bottom ist immer Top berechnen kann, eine beliebige Anzahl an eine beliebige Anzahl, da das Hinzufügen immer eine willkürliche
Anzahl
• plus(+, +) ist +, weil das Hinzufügen von zwei positiven Zahlen immer eine positive Zahl ergibt
• plus(-, -) ist -, weil das Hinzufügen von zwei negativen Zahlen immer eine negative Zahl ergibt
• plus(0, x), x != Bottom ist x, weil 0 die Identität der Addition ist.

Das Problem ist, dass

• plus - +Top sein, weil Sie nicht wissen, ob es sich um eine positive oder negative Zahl ist.

So statisch sicher sein, würden Sie die konservative Ansatz müssen und eine solche Operation nicht zulassen.

Es gibt , aber letztendlich leiden alle unter dem gleichen Problem: Sie stellen eine Überlappung mit dem tatsächlichen Programmzustand dar.

Ich würde sagen, das Problem ist ähnlich wie Integer Überlauf/Unterlauf: Im Allgemeinen wissen Sie nicht statisch, ob eine Operation einen Überlauf aufweist - Sie wissen nur zur Laufzeit.

Answer 2

Es könnte möglich sein, wenn SIP-23 implementiert wurde, mit impliziten Parametern als eine Form der Verfeinerungstypen. Es wäre jedoch von fragwürdigem Wert, obwohl das Scala-Compiler- und -Typsystem nicht wirklich gut dafür geeignet ist, interessante Dinge über beispielsweise ganze Zahlen zu beweisen.Dafür wäre es viel netter, eine Sprache mit abhängigen Typen (Idris etc.) oder Verfeinerungsarten zu verwenden, die von einem SMT-Solver (LiquidHaskell etc.) geprüft werden.