Типы и литералы на основе ограничений Scala

Question

Я думал, можно ли в Scala определить тип, например NegativeNumber. Этот тип будет представлять собой отрицательное число, и это будет проверено компилятором аналогично Ints, струнные и т.д.

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

Аналогично:

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

я мог бы использовать эти типы так же, как другие типы, например:

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

Эти ограниченные типы могут поддерживаться случайными типами (Int, String).

Возможно ли реализовать эти типы (возможно, с помощью макросов)?

Как насчет пользовательских литералов?

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

Answer 1

К сожалению, это не то, что вы могли бы легко проверить во время компиляции. Ну, по крайней мере, нет, если вы не ограничиваете операции над своим типом. Если ваша цель - просто проверить, что числовой литерал отличен от нуля, вы можете легко написать макрос, который проверяет это свойство. Однако я не вижу никакой пользы в доказательстве того, что отрицательный литерал действительно отрицательный.

Проблема не является ограничением Scala - которая имеет очень сильную систему типов, но тот факт, что (в достаточно сложной программе) вы не можете статически знать все возможные состояния. Однако вы можете попытаться переопределить набор всех возможных состояний.

Рассмотрим пример введения типа NegativeNumber, который только когда-либо представляет отрицательное число. Для простоты мы определяем только одну операцию: plus.

Предположим, вы допустили бы только добавление нескольких NegativeNumber, тогда система типов может быть использована для гарантии того, что каждый NegativeNumber действительно является отрицательным числом. Но это кажется действительно ограничительным, поэтому полезный пример, безусловно, позволит нам добавить, по крайней мере, NegativeNumber и общий Int.

Что делать, если у вас было выражение val z: NegativeNumber = plus(x, y), где вы не знаете значения x и y статически (возможно, они возвращаются функцией). Как вы знаете (статически), что z is indead отрицательное число?

подход к решению этой проблемы было бы ввести Abstract Interpretation, который должен быть запущен на представлении вашей программы (Source Code, Abstract Syntax Tree, ...).

Например, вы могли бы определить Решетку на номера со следующими элементами:

• Top: все номера
• +: все положительные числа
• 0: число 0
• -: все отрицательные числа
• Bottom: не число - только ввел, что каждая пара элементов имеет наибольшую нижнюю границу

с упорядочением Top> (+, 0, -)>Bottom.

Затем вам нужно определить семантику для операций. Принимая коммутативную метод plus из нашего примера:

• plus(Bottom, something) всегда Bottom, так как вы не можете вычислить что-то с помощью недопустимых номеров
• plus(Top, x), x != Bottom всегда Top, потому что добавление произвольного числа на любое число всегда произвольное номер
• plus(+, +) является +, потому что добавление двух положительных чисел всегда будет давать положительное число
• plus(-, -) является -, так как добавление двух отрицательных чисел всегда будет давать отрицательное число
• plus(0, x), x != Bottom - x, потому что 0 является личностью добавления.

Проблема заключается в том, что

• plus - + будет Top, потому что вы не знаете, если это положительное или отрицательное число.

Так быть статически безопасным, вы должны принять консервативный подход и запретить такую ​​операцию.

Есть more sophisticated numerical domains, но в конечном итоге все они страдают от одной и той же проблемы: они представляют собой чрезмерное приближение к фактическому состоянию программы.

Я бы сказал, что проблема похожа на целочисленное переполнение/недополнение: Как правило, вы не знаете, статически ли операция демонстрирует переполнение - вы это знаете только во время выполнения.

Answer 2

Было бы возможно, если бы была реализована SIP-23 с использованием неявных параметров как формы уточняющих типов. Тем не менее, это было бы сомнительным, хотя, поскольку Scala-компилятор и система типов на самом деле не очень хорошо оснащены для доказательства интересных вещей, например, целых чисел.Для этого было бы гораздо лучше использовать язык с зависимыми типами (Idris и т. Д.) Или типы уточнения, проверенные решателем SMT (LiquidHaskell и т. Д.).