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

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

0 голосов
/ 23 октября 2018

Я все еще пытаюсь понять, как разделить код при использовании 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).Если бы кто-то мог объяснить, что происходит, и в идеале способ обойти это, было бы здорово.Конечно, я мог бы просто потратить некоторое время, но лучше понять эти чертовы модули.Спасибо!

1 Ответ

0 голосов
/ 23 октября 2018

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

, которые дают то же самоеerror as yours:

Error: Это выражение имеет тип (модуль 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
...