Есть ли в Scala ограничение по значению, такое как ML, если нет, то почему?

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

let r : ∀A.Ref(List(A)) = ref [] in
r := ["boo"];
head(!r) + 1

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

Следовательно, когда вы добавляете ссылки на F ‹: тогда вам нужно наложить ограничение на значение, чтобы не потерять разумность. Точно так же MLsub не может избавиться от ограничения значения. Scala уже применяет ограничение значения через свой синтаксис, поскольку нет возможности даже написать определение значения, которое имело бы полиморфный тип.

Все намного проще. В Scala значения не могут иметь полиморфные типы, могут только методы. Например. если вы напишете

val id = x => x

его тип не [A] A => A.

И если вы возьмете полиморфный метод, например

 def id[A](x: A): A = x

и попробуйте присвоить ему значение

 val id1 = id

снова компилятор попытается (и в этом случае не удастся) вывести конкретное A вместо создания полиморфного значения.

Так что проблемы не возникает.

РЕДАКТИРОВАТЬ:

Если вы попытаетесь воспроизвести пример http://mlton.org/ValueRestriction#_alternatives_to_the_value_restriction в Scala, проблема, с которой вы сталкиваетесь, заключается не в отсутствии let: val ей прекрасно соответствует. Но вам понадобится что-то вроде

val f[A]: A => A = {
  var r: Option[A] = None
  { x => ... }
}

что незаконно. Если вы пишете def f[A]: A => A = ..., это допустимо, но при каждом вызове создается новый r. В терминах машинного обучения это выглядело бы как

val f: unit -> ('a -> 'a) =
    fn () =>
       let
          val r: 'a option ref = ref NONE
       in
          fn x =>
          let
             val y = !r
             val () = r := SOME x
          in
             case y of
                NONE => x
              | SOME y => y
          end
       end

val _ = f () 13
val _ = f () "foo"

что разрешено ограничением стоимости.

То есть правила Scala эквивалентны разрешению только лямбда-выражений в качестве полиморфных значений в ML вместо всего, что позволяет ограничение значений.

РЕДАКТИРОВАТЬ: этот ответ был неверно до. Я полностью переписал приведенное ниже объяснение, чтобы получить свое новое понимание из комментариев под ответами Андреаса и Алексея.

_{История редактирования и история архивов этой страницы на archive.is содержат запись моего предыдущего недоразумения и обсуждения. Еще одна причина, по которой я решил отредактировать, а не удалить и написать новый ответ, - это сохранить комментарии к этому ответу. ИМО, этот ответ по-прежнему необходим, потому что, хотя Алексей отвечает на заголовок темы правильно и кратко - также разработка Андреаса была для меня наиболее полезной для понимания - все же я думаю, что непрофессиональному читателю может потребоваться другой, более целостный (но, надеюсь, все же генеративная сущность) объяснение, чтобы быстро получить некоторую глубину понимания проблемы. Также я думаю, что другие ответы неясны, насколько запутанным является целостное объяснение, и я хочу, чтобы у наивных читателей была возможность попробовать его на вкус. Предыдущие разъяснения, которые я нашел, не содержат всех деталей на английском языке, а вместо этого (как математики обычно делают для повышения эффективности) полагаются на читателя, чтобы различить детали из нюансов примеров символического языка программирования и необходимых знаний предметной области ( например, общие сведения о дизайне языков программирования).}

Ограничение значения возникает, когда у нас есть изменение ссылочных ¹ параметризованных объектов типа ². Небезопасность типа, которая может возникнуть без ограничения значения, продемонстрирована в следующем примере кода MLton:

val r: 'a option ref = ref NONE
val r1: string option ref = r
val r2: int option ref = r
val () = r1 := SOME "foo"
val v: int = valOf (!r2)

Значение NONE (которое похоже на null), содержащееся в объекте, на который ссылается r, может быть присвоено ссылке с любым конкретным типом для параметра типа 'a, потому что r имеет полиморфный тип a'. Это сделает тип небезопасным, потому что, как показано в примере выше, тот же объект, на который ссылается r, который был назначен как для string option ref, так и для int option ref, может быть записан (т. Е. Изменен) со значением string через ссылку r1, а затем прочитан как значение int. по ссылке r2. Ограничение значения вызывает ошибку компилятора для приведенного выше примера.

Сложность ввода возникает для предотвращения ³ (повторной) количественной оценки (т.е. привязки или определения) параметра типа (также известного как переменная типа) указанной ссылки (и объекта, на который она указывает) для типа который отличается при повторном использовании экземпляра указанной ссылки, который ранее был количественно определен другим типом.

Такие (возможно, сбивающие с толку и запутанные) случаи возникают например, где последовательные приложения-функции (также известные как вызовы) повторно используют один и тот же экземпляр такой ссылки. IOW, случаи, когда параметры типа (относящиеся к объекту) для ссылки (повторно) количественно оцениваются каждый раз при применении функции, все же экземпляр ссылки (и объект, на который он указывает ) повторно используется для каждого последующего применения (и количественной оценки) функции.

Кстати, их появление иногда бывает не интуитивно из-за отсутствия явный универсальный квантификатор ∀ (поскольку неявный ранг-1 предшествующий лексический количественную оценку области можно исключить из лексического порядка оценки с помощью таких конструкций, как let или сопрограммы) и, возможно, большей нерегулярности (по сравнению со Scala) того, когда могут возникнуть небезопасные случаи в ограничении значений ML:

Андреас написал :

Повторное использование объекта ссылки, например, желательно для let выражений, которые аналогичны математической нотации, должны создавать и оценивать создание замен только один раз, даже если они могут быть лексически заменены более одного раза в пределах предложения in. Итак, например, если приложение-функция оценивается как (независимо от того, является ли оно также лексическим или нет) в предложении in, в то время как параметры типа замен повторно количественно оцениваются для каждого приложения (поскольку создание экземпляров замен выполняется только лексически внутри приложения-функции), тогда безопасность типа может быть потеряна, если все приложения не вынуждены проводить количественную оценку параметров типа-нарушителя только один раз (т. е. не позволяют параметру типа-нарушителю быть полиморфным).

Scala делает синтаксическим ограничением против всего такого ссылки, что является компромиссом, ограничивающим например, тот же и даже больше случаев (которые были бы безопасны, если не ограничивать), чем ограничение значения ML, но более регулярное в том смысле, что мы не будем ломать голову над сообщение об ошибке, относящееся к ограничению значения. В Scala мы никогда не разрешал создавать такую ​​ссылку. Таким образом, в Scala мы можем только в явных случаях, когда новый экземпляр ссылки создается при количественной оценке параметров типа. Примечание. OCaml расслабляет ограничение значения в некоторых случаях.

Обратите внимание, что как Scala, так и ML не позволяют объявить ссылку неизменной ¹, хотя объект, на который они указывают, можно объявить неизменяемым с помощью val. Обратите внимание, что нет необходимости вводить ограничения для ссылок, которые нельзя изменять.

Причина, по которой изменяемость ссылочного типа ¹ требуется для возникновения сложных случаев типизации, заключается в том, что если мы создаем экземпляр ссылки (например, в предложении замен let) с не- параметризованный объект (т.е. не None или Nil ⁴, а вместо этого, например, Option[String] или List[Int]), тогда ссылка не будет иметь полиморфного типа (относящегося к объекту, на который он указывает), и поэтому проблема повторной количественной оценки никогда не возникает. Таким образом, проблемные случаи возникают из-за создания экземпляра с полиморфным объектом, а затем последующего присвоения нового количественно определенного объекта (т. Е. Изменения ссылочного типа) в повторно количественно определенном контексте с последующим разыменованием (чтением) из (объект, на который указывает) ссылка в последующем повторно количественный контекст. Как упоминалось выше, когда повторно квантифицированные параметры типа конфликтуют, возникают сложности с типизацией, и небезопасные случаи должны быть предотвращены / ограничены.

Фух! Если вы поняли это, не просматривая связанные примеры, я впечатлен.

¹ _{ИМО, чтобы вместо этого использовать фразу «изменяемые ссылки» вместо «изменчивость ссылочного объекта» и «изменчивость ссылочного типа» было бы более потенциально запутанным, потому что наше намерение состоит в том, чтобы изменить значение объекта (и его тип), на которое ссылается указатель, - не относящиеся к изменчивости указателя того, на что указывает ссылка. Некоторые языки программирования даже не различают явно, когда они запрещают, в случае примитивные типы: выбор изменения ссылки или объекта, на который они указывают.}

² _{При этом объект может даже быть функцией на языке программирования, который позволяет выполнять функции первого класса.}

³ _{Чтобы предотвратить ошибку сегментации во время выполнения из-за доступа (чтения или записи) к указанному объекту с предположением о его статически (то есть во время компиляции) определенном типе, который не является типом что объект действительно имеет.}

⁴ _{Какие NONE и [] соответственно в ML.}

Извините за аргумент, но синтаксис Scala не мешает мне писать val r: 'a option ref = ref NONE val r1: string option ref = r val r2: int option ref = r val () = r1 := SOME "foo" val v: int = valOf (!r2) , а скорее проверщик типов жалуется, что «не найдено: тип A». Тем не менее, Scala не применяет другие ограничения значений, которые можно увидеть в ML, как, например, когда я успешно скомпилировал в REPL NONE null.