Próbuję zbudować hierarchię typów modułów, które zależą od siebie. W COQ mogę napisać coś takiego:

Module Type Foo.
  Parameter t:Type.
End Foo.

Module Type Bar1 (T:Foo).
  Parameter f1: T.t -> T.t.
End Bar1.

Module Type Bar2 (T:Foo).
  Parameter f2: T.t -> T.t.
End Bar2.

Module Ex (F:Foo) (B1: Bar1 F) (B2:Bar2 F).

End Ex.

Jak wyrażałbym to w Ocaml?

4
krokodil 19 luty 2018, 22:19

3 odpowiedzi

Najlepsza odpowiedź

Aby opracować odpowiedź GSG, jeśli masz bardziej złożony typ modułu Foo, możesz użyć with module zamiast with type i mieć specyfikację modułu w typach Bar, Podobnie jak w następnym przykładzie:

module type Foo =
sig
  type t
end

module type Bar1 = sig
  module F: Foo
  val f1: F.t -> F.t
end

module type Bar2 = sig
  module F: Foo
  val f2: F.t -> F.t
end

module Ex (F: Foo) (B1: Bar1 with module F = F) (B2: Bar2 with module F = F) =
struct

let f3 x = B2.f2 (B1.f1 x)

end

module Bar1_impl (F: Foo): Bar1 with module F = F = struct
  module F = F
  let f1 x = x
end

module Bar2_impl (F: Foo): Bar2 with module F = F = struct
  module F = F
  let f2 x = x
end

module F: Foo with type t = int = struct type t = int end

module M = Ex(F)(Bar1_impl(F))(Bar2_impl(F))

let x = M.f3 0;;
2
Virgile 20 luty 2018, 08:13

Niestety, OCAML nie obsługuje bezpośrednio parametryzowanych typów modułów. Można jednak naśladować je przez owijanie parametryzowanego modułu wokół nich:

module type Foo =
sig
  type t
end

module Bar (X : Foo) =
struct
  module type T =
  sig
    val f : X.t -> X.t
  end
end

module Ex (F : Foo) (B : Bar(F).T) = ...

Nieco bardziej niezdarny, ale ma taki sam efekt.

5
Andreas Rossberg 19 luty 2018, 21:01

Typy modułów nie biorą argumentów. Jednak ten szczególny wzór można wyrazić przez with type:

module type FOO = sig
  type t
end

module type BAR1 = sig
  type t
  val f1 : t -> t
end

module type BAR2 = sig
  type t
  val f2 : t -> t
end

module Ex (F:FOO) (B1 : BAR1 with type t = F.t) (B1 : BAR2 with type t = F.t) = struct
end
2
gsg 19 luty 2018, 19:47