Кодировать эквивалент полиморфизма ранга 2 в SML

runST — это функция Haskell, которая статически ограничивает время жизни ресурса с помощью типов. Для этого используется полиморфизм второго ранга. Более простая система типов стандартного ML предлагает только полиморфизм ранга 1.

Может ли Standard ML по-прежнему использовать типы, чтобы ограничить время жизни ресурса аналогичными конечными результатами?

Эта страница и эта страница демонстрирует некоторые способы реструктуризации кода для использования только более простых типов. Если я правильно понимаю, ядро ​​состоит в том, чтобы обернуть выражение так, чтобы оно было заменено его возможными наблюдениями в контексте, которые конечны. Является ли эта техника универсальной? Можно ли использовать его или связанную с ним кодировку с чем-то подобным (очевидно, не идентичным по сигнатуре) runST, чтобы предотвратить наблюдение за типом выхода значения из обернутого выражения? Если да, то как?

Сценарий, который я себе представляю, примерно такой:

magicRunSTLikeThing (fn resource =>
    (* do things with resource *)
    (* return a value that most definitely doesn't contain resource *)
)

...где magic... предоставляет ресурс, который пользовательскому коду невозможно использовать каким-либо образом. Очевидно, что такой простой интерфейс с одной библиотечной функцией невозможен, но, возможно, с различными слоями упаковки, ручного встраивания и извлечения...?

Я видел это, но если я правильно понял (... скорее всего, нет) , что на самом деле не предотвращает совместное использование всех ссылок на ресурс, а только гарантирует, что одна ссылка на него должна быть "закрыта".

По сути, я хочу реализовать безопасные типизированные явные области (не выведенные в стиле MLKit) в SML.


haskell higher-rank-types sml hindley-milner ml
person Leushenko    schedule 10.06.2014    source источник

Ответы (1)


arrow_upward
2
arrow_downward

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

Можно (я думаю) использовать генеративные типы данных и функторы SML для создания абстрактных фантомных типов, на которые нельзя ссылаться за пределами данного лексического блока:

datatype ('s, 'a) Res = ResC of 's

signature BLOCK = sig
  type t
  val f:('s, t) Res -> t
end

signature REGION = sig
  type t
  val run:unit -> t
end

functor Region(B:BLOCK) :> REGION where type t = B.t = struct
  type t = B.t
  datatype phan = Phan
  fun run () = let
    val ret = (print "opening region\n"; B.f(ResC Phan))
  in print "closing region\n" ; ret end
end

structure T = Region(struct
  type t = int
  fun f resource = ( (* this function forms the body of the "region" *)
    6
  )
end)

;print (Int.toString(T.run()))

Это не позволяет программе просто возвращать resource или объявлять внешние изменяемые переменные, которым она может быть назначена, что решает большую часть проблемы. Но он все еще может быть закрыт функциями, созданными в блоке «регион», и сохранен таким образом после предполагаемой точки закрытия; такие функции можно экспортировать, а оборванную ссылку на ресурс использовать снова, вызывая проблемы.

Однако мы можем сымитировать ST и запретить замыканиям делать что-либо полезное с resource, заставив область использовать монаду с ключом фантомного типа:

signature RMONAD = sig
  type ('s, 'a, 'r) m
  val ret: ('s * 'r) -> 'a -> ('s, 'a, 'r) m
  val bnd: ('s, 'a, 'r) m * ('a * 'r -> ('s, 'b, 'r) m) -> ('s, 'b, 'r) m
  val get: 's -> ('s, 'a, 'r) m -> 'a * 'r
end

structure RMonad :> RMONAD = struct
  type ('s, 'a, 'r) m = 's -> 's * 'a * 'r
  fun ret (k, r) x = fn _ => (k, x, r)
  fun bnd (m, f) = fn k => let
    val (_, v, r) = m k
  in f (v, r) k end
  fun get k m = let val (_, v, r) = m k in (v, r) end
end

signature MBLOCK = sig
  type t
  val f:(t -> ('s, t, 'r) RMonad.m)  (* return *)
         * ('r -> ('s, string, 'r) RMonad.m) (* operations on r *)
        -> ('s, t, 'r) RMonad.m
end

signature MREGION = sig
  type t
  val run:unit -> t
end

functor MRegion(B:MBLOCK) :> MREGION where type t = B.t = struct
  type t = B.t
  datatype phan = Phan
  fun run () = let
    val (ret, res) = RMonad.get Phan (B.f(RMonad.ret(Phan, "RESOURCE"),
                                     (fn r => RMonad.ret(Phan, "RESOURCE") r)))
  in
    print("closing " ^ res ^ "\n") ; ret
  end
end

structure T = MRegion(struct
  type t = int
  fun f (return, toString) = let
    val >>= = RMonad.bnd
    infix >>=
  in
    return 6 >>= (fn(x, r) =>
      toString r >>= (fn(s, r) => (
        print ("received " ^ s ^ "\n");
        return (x + 1)
    )))
  end
end)

;T.run()

(это беспорядок, но он показывает мою основную идею)

Ресурс берет на себя роль STRef; если все предоставленные операции над ним возвращают монадическое значение вместо того, чтобы работать напрямую, он создаст цепочку отложенных операций, которые могут быть выполнены только путем возврата к run. Это противодействует способности замыканий сохранять копию r вне блока, потому что они никогда не смогут фактически выполнить цепочку операций, не смогут вернуться к run и, следовательно, не смогут получить к ней доступ каким-либо образом.

Вызов T.run дважды приведет к повторному использованию одного и того же типа «ключа», что означает, что это не эквивалентно вложенному forall, но это не должно иметь значения, если нет способа разделить r между двумя отдельными вызовами; которого нет - если он не может быть возвращен, не может быть назначен снаружи, и любые замыкания не могут запускать код, который на нем работает. По крайней мере, я так думаю.

person Leushenko    schedule 18.10.2014