Parametrycznie lokalnie abstrakcyjny typ

Question

Próbuję dowiedzieć się, jak napisać funkcję w zależności od modułu z parametrowym typem, ale nie mogę znaleźć niczego podobnego w dowolnym miejscu. Starałem się maksymalnie ograniczyć problem i skończyłem z tym fałszywym przykładem.

module type Mappable = sig 
    type 'a t 
    val map : ('a -> 'b) -> 'a t -> 'b t 
end 

let plus (type m) (module M : Mappable with type 'a t = 'a m) (xs : int m) = 
    M.map (fun x -> x + 1) xs 

która podaje błąd Error: Syntax error: module-expr expected.

Jeśli upuszczę 'a, otrzymam następujący błąd.

Error: In this `with' constraint, the new definition of t 
     does not match its original definition in the constrained signature: 
     Type declarations do not match: type t is not included in type 'a t 
     They have different arities. 

Jaka jest prawidłowa składnia w tym celu?

Answer 1

Wierzę, że to, co chcesz zrobić, jest niemożliwe w OCaml 4.02.3. Zobaczmy uproszczoną wersję bez zmiennej typu:

module type Mappable = sig 
    type t 
    val map : ('a -> 'b) -> t -> t 
end 

let plus (type m) (module M : Mappable with type t = m) (xs : m) = 
    M.map (fun x -> x + 1) xs 

Powyższe oznaczalnych izolatów i plus posiada następujące rodzaje:

val plus : (module Mappable with type t = 'm) -> 'm -> 'm 

typ m w swej definicji są wydobywane do zmiennej 'm.

Teraz wróć do oryginalnego kodu i zastanów się, jaki typ powinien mieć typ plus. Ponieważ staramy się abstrakcyjnego m przez (type m), powinno być:

val plus : (module Mappable with type 'a t = 'a 'm) -> 'a 'm -> 'a 'm 

Niestety OCaml nie obsługuje wyższą kinded polimorfizmu który pozwala tej formy typu 'a 'm. Wydaje się, że pierwszorzędne pisanie modułów jest starannie realizowane, aby go nie wprowadzać.

Możesz zobaczyć następujący krótki artykuł, który wyjaśnia obecny (niefortunny) status wyższego rodzaju polimorfizmu w OCaml. Wyjaśnia to obejście: Jak zakodować go w obecnych ramach OCaml z kosztów jawnych coersions:

https://ocamllabs.github.io/higher/lightweight-higher-kinded-polymorphism.pdf

nigdy nie próbowałem sam, ale to samo obejście można zastosować do przykładu.

Answer 2

Nie jest to możliwe w SML, jako rodzaj ograniczenie nie jest regularny typ modułu przymus, ale specjalny syntactic construct, który nie pozwala polimorficzne typy:

Pakiet typu składniowym występując w klasie wyrażenie typu (typ-modułu-pakietu) oraz w postaciach z adnotacjami reprezentuje podzbiór typów modułów. Ten podzbiór składa się z nazwanych typów modułów z opcjonalnymi ograniczeniami o ograniczonej formie: można określić tylko typy nieparametryczne.

zwykły Rozwiązaniem byłoby utworzyć moduł, który wiąże wszystkie zmienne typu do konkretnych typów:

module type Mapper = sig 
    type a 
    type b 
    type src 
    type dst 
    val map : (a -> b) -> src -> dst 
end 

let plus (type src) (type dst) 
    (module M : Mapper with type dst = dst 
         and type src = src 
         and type a = int 
         and type b = int) (xs : src) : dst = 
    M.map (fun x -> x + 1) xs 

w danym przykładzie, nie ma potrzeby, aby związać 'a i 'b, ponieważ są one zasadniczo nie są używane, więc można uprościć do:

module type Mapper = sig 
    type src 
    type dst 
    val map : ('a -> 'b) -> src -> dst 
end 

let plus (type src) (type dst) 
    (module M : Mapper with type dst = dst 
         and type src = src) (xs : src) : dst = 
    M.map (fun x -> x + 1) xs 

oczywiście, to jest bardzo ograniczające, ale to, co jest możliwe do dnia.

Answer 3

Jeśli chcesz przekazać moduły do ​​funkcji, należy użyć funktory Zamiast:

module F (M : Mappable) = struct 
    let plus xs = M.map (fun x -> x + 1) xs 
end