Как сопоставить модули с типом модуля в OCaml?

Question

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

Вот пример того, чтоЯ хотел бы сделать:

module type Field =
sig
  type t
  val add : t -> t -> t
  val mul : t -> t -> t
end

module type Func (F1 : Field) (F2 : Field) =
sig
  val eval : F1.t -> F2.t
end

module FuncField (F1 : Field) (F2 : Field) (F : Func F1 F2) =
struct
  let eval a = F.eval a
  let add a b = F2.add (F.eval a) (F.eval b)
  let mul a b = F2.mul (F.eval a) (F.eval b)
end

У меня есть тип модуля Field, например, действительные и рациональные числа, и я хочу определить тип функций Func от одного поля додругой, который равен F1.t -> F2.t для любых двух заданных модулей F1, F2.С этими типами модулей я могу определить FuncField, который принимает F1, F2, F и в основном увеличивает F.eval с add и mul.

КогдаЯ запускаю код, я получаю общий Error: Syntax error в строке, где я определяю Func.Есть ли способ определить что-то подобное в OCaml?

Я не уверен, требуются ли для этого зависимые типы, но я слегка знаком с Coq, у которого есть зависимые типы, и он не жаловался, когдаЯ определил эквивалентную конструкцию:

Module Type Field.
  Parameter T : Type.
  Parameter add : T -> T -> T.
  Parameter mul : T -> T -> T.
End Field.

Module Type Func (F1 : Field) (F2 : Field).
  Parameter eval : F1.T -> F2.T.
End Func.

Module FuncField (F1 : Field) (F2 : Field) (F : Func F1 F2).
  Definition eval a := F.eval a.
  Definition add a b := F2.add (F.eval a) (F.eval b).
  Definition mul a b := F2.mul (F.eval a) (F.eval b).
End FuncField.

Answer 1

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

module type Field =
sig
  type t
  val add : t -> t -> t
  val mul : t -> t -> t
end

module type Func =
sig
  type t1
  type t2
  val eval : t1 -> t2
end

module FuncField (F1 : Field) (F2 : Field) (F : Func with type t1 = F1.t and type t2 = F2.t) =
struct
  let eval a = F.eval a
  let add a b = F2.add (F.eval a) (F.eval b)
  let mul a b = F2.mul (F.eval a) (F.eval b)
end

Answer 2

Функторы - это функции от модулей к модулям.Функтора от типа модуля к типу модуля не существует ... но вы можете обмануть.:)

В отличие от Coq, модули OCaml не являются полностью зависимыми типами, но в этом случае они "достаточно зависимы".Идея состоит в том, что модули могут содержать типы модулей.Поскольку мы не можем вернуть тип модуля напрямую, мы просто вернем модуль, который его содержит!

Ваш пример станет таким:

module type Field = sig
  type t
  val add : t -> t -> t
  val mul : t -> t -> t
end

module Func (F1 : Field) (F2 : Field) = struct
  module type T = sig
    val eval : F1.t -> F2.t
  end
end

module FuncField (F1 : Field) (F2 : Field) (F : Func(F1)(F2).T) = struct
  let eval a = F.eval a
  let add a b = F2.add (F.eval a) (F.eval b)
  let mul a b = F2.mul (F.eval a) (F.eval b)
end

Обратите внимание на синтаксис Func(F1)(F2).T, которыйговорит "примените функтор, и из результата возьмите модуль типа T".Эта комбинация приложения функтор + доступ к полю доступна только в типах (нормальных или модульных).

Я не помню, где я нашел этот трюк первым, но вы можете увидеть его в действии "на производстве"в tyxml ( определение , использование ).