Подпись для этого упакованного модуля не может быть выведена в рекурсивной функции

Question

Я все еще пытаюсь понять, как разделить код при использовании mirage, и это множество модулей первого класса. Я положил все, что мне нужно, в большой урод Context модуль, чтобы не передавать десять модулей всем моим функциям, достаточно одного.

У меня есть функция для получения команд через TCP:

let recvCmds (type a) (module Ctx : Context with type chan = a) nodeid chan = ...

После нескольких часов проб и ошибок я понял, что мне нужно добавить (type a) и "явный" type chan = a чтобы это работало. Выглядит некрасиво, но компилируется. Но если я хочу сделать эту функцию рекурсивной:

let rec recvCmds (type a) (module Ctx : Context with type chan = a) nodeid chan =
  Ctx.readMsg chan >>= fun res ->
  ... more stuff ...
  |> OtherModule.getStorageForId (module Ctx)
  ... more stuff ...
  recvCmds (module Ctx) nodeid chan

Я передаю модуль дважды, первый раз без проблем, но я получаю сообщение об ошибке в строке рекурсии:

The signature for this packaged module couldn't be inferred.

и если я пытаюсь указать подпись, я получаю

This expression has type a but an expression was expected of type 'a
The type constructor a would escape its scope

И кажется, что я не могу использовать весь (type chan = a) вещь. Если бы кто-то мог объяснить, что происходит, и в идеале, как обойти это, было бы здорово. Конечно, я мог бы использовать какое-то время, но я бы, наконец, понял эти чертовы модули. Спасибо!

Answer 1

Практический ответ заключается в том, что рекурсивные функции должны повсеместно количественно определять свои локально абстрактные типы с let rec f: type a. .... = fun ...,

Точнее, ваш пример можно упростить до

module type T = sig type t end 
let rec f (type a) (m: (module T with type t = a)) = f m

которые дают ту же ошибку, что и ваша:

Ошибка: это выражение имеет тип (модуль T с типом t = a), но ожидалось выражение типа 'a Конструктор типа a выйдет из своей области видимости

Эта ошибка может быть исправлена ​​с помощью явного полного количественного определения: это можно сделать с помощью сокращенной записи (для универсально выраженного локально абстрактного типа):

let rec f: type a.  (module T with type t = a) -> 'never = fun m -> f m

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

let ext_store = ref None
let store x = ext_store := Some x
let f (type a) (x:a) = store x

должен явно потерпеть неудачу, потому что он пытается сохранить значение типа a, который является бессмысленным типом вне тела f,

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

  let id x = x
  let f (x:a) : a = id x

хорошо, потому что id x работает для любого x,

Проблема с такой функцией, как

 let rec f (type a) (m: (module T with type t = a)) = f m

то тип f еще не обобщен внутри своего тела, потому что обобщение типа в ML происходит в let определение. Поэтому исправление заключается в явном указании компилятору, что f полиморфен в своем аргументе:

 let rec f: 'a. (module T with type t = 'a) -> 'never =
   fun (type a) (m:(module T with type t = a)) -> f m

Вот, 'a. ... это универсальное количественное определение, которое следует читать forall 'a. ..., Эта первая строка сообщает компилятору, что функция f полиморфен в своем первом аргументе, тогда как вторая строка явно вводит локально абстрактный тип a для уточнения типа упакованного модуля. Разделение этих двух объявлений довольно многословно, поэтому сокращенная запись объединяет оба:

let rec f: type a.  (module T with type t = a) -> 'never = fun m -> f m