Монады и ограничение значений в ML

Ограничение значений в 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 монады, остаются мономорфными на протяжении всей последовательности, поэтому, похоже, достигается тот же эффект, что и ограничение значения, без введения особых случаев во время обобщения.

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


monads ml value-restriction
person max    schedule 22.10.2016    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Да, в основном это работает, и именно так работает Haskell. Однако есть загвоздка: вы должны убедиться, что ссылка никогда не «ускользает» от монады. Псевокод:

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

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

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, и требуется расширение langugae (Rank2Types) в Haskell.

person zenhack    schedule 30.10.2017
comment
Большое спасибо за подробный ответ! Тем временем я также наткнулся на runST и его необходимость, но не был уверен, будет ли это гарантировать надежность. Заинтересованные читатели могут также проверить этот связанный вопрос. - person max; 31.10.2017