OCaml: проблема с конструктором типов, выходящим из его области видимости - PullRequest
Новая
       14

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

1 голос
/ 07 марта 2019

Вот код: 

module type S = sig
  type t
  val do_it: t -> int -> t
end

let rec foo (type a) (module Foo:S with type t=a) (i:int) (x:a) = 
  if i=0 then x
  else foo (i-1) (Foo.do_it x i)

Я получаю ошибку этого типа (в строке 8, символы 17-32): 

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

Что является неожиданным, поскольку конструктор типа a все еще находится в своей области видимости. Я ожидаю, что функция foo будет иметь следующий тип: 

foo: (module S with type t = 'a) -> int -> 'a -> 'a

Что не так?

1 Ответ

3 голосов
/ 07 марта 2019

Проблема заключается в полиморфной рекурсии: функция foo не может быть полиморфной в своем теле без явной аннотации. При написании 

let rec foo (type a) (module Foo:S with type t=a) (i:int) (x:a) = 
  if i=0 then x
  else foo (module Foo:S with type t = a) (i-1) (Foo.do_it x i)

, поскольку функция foo не является полиморфной в своем определении, она не может повторно использовать локально абстрактный тип type a, который был введен после ее собственного определения.

Один из способов обойти эту проблему - ввести рекурсивную функцию после локально абстрактного типа: 

let foo (type a) =
  let rec foo (module Foo:S with type t=a) (i:int) (x:a) = 
  if i=0 then x
  else foo (module Foo) (i-1) (Foo.do_it x i) in
  foo

Более классическим решением является добавление явного универсального количественного определения к локально абстрактному типу a: 

let rec foo: type a. (module S with type t=a) -> int -> a -> a =
fun (module Foo) i x ->
  if i=0 then x
  else foo (module Foo) (i-1) (Foo.do_it x i)
...