Монады и ценностное ограничение в ОД

Question

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

let x = ref [];;  (* value restriction prevents generalization here *)

x := 1::!x;;      (* type unification with int *)
x := true::!x;;   (* error *)

Без ограничения значения последняя строка проверила бы тип без ошибки, так как полиморфный тип для x объединится с bool, Чтобы предотвратить это, введите x должен оставаться мономорфным.

Мой вопрос заключается в следующем: возможно ли снять ограничение по значению, используя монады для выражения последовательности операций?

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

Будет ли это работать, а если нет, то почему?

Answer 1

Да, это в основном работает, и именно так Хаскель делает вещи. Однако есть одна проблема: вы должны убедиться, что ссылка никогда не "ускользает" от монады. Psuedocode:

module MutMonad : sig
  (* This is all sound: *)
  type 'a t
  type 'a ref

  val mkref : 'a -> ('a ref) t
  val read_ref : 'a ref -> 'a t
  val write_ref : 'a -> 'a ref -> unit t

  (* This breaks soundness: *)
  val run : 'a t -> 'a
end

Существование пробега возвращает нас туда, откуда мы начали:

let x = run (mkref []) in (* x is of type ('a list) ref *)
run (read_ref x >>= fun list -> write_ref (1::list) x);
run (read_ref x >>= fun list -> write_ref (true::list) x)

Haskell справляется с этим двумя способами:

• поскольку main это уже монадический тип (IO), он может просто не иметь runIO или подобного.
• Монада ST использует прием с типами ранга 2, чтобы гарантировать, что ссылки не будут использоваться после выхода из монады, что позволяет локально изменяемое состояние при сохранении звука.

Для второго случая у вас есть что-то вроде:

module MutMonad : sig
  (* The types now take an extra type parameter 's,
     which is a phantom type. Otherwise, the first
     bit is the same: *)
  type 'a 's t
  type 'a 's ref

  val mkref : 'a -> ('a 's ref) 's t
  val read_ref : 'a 's ref -> 'a 's t
  val write_ref : 'a -> 'a 's ref -> unit 's t

  (* This bit is the key. *)
  val run : (forall 's. 'a 's t) -> 'a
end

forall 's. ... на уровне типа является аналогом fun x -> ..., 's локально связана с переменной, так что аргумент для запуска не может предполагать ничего о' s. В частности, это не будет проверка типа:

let old_ref = run (mkref 3) in
run (read_ref old_ref)

Поскольку аргументы для запуска не могут предполагать, что они переданы одного типа для 's,

Для этого требуется особенность системы типов, которой нет в ocaml, а также расширение языка (Rank2Types) в Haskell.