Стирания параметр типа

Question

У меня есть модуль гнездо с использованием типов фантомных для обеспечения некоторого простого контроля доступа:

module Socket : sig 
    type 'a t 

    val ro : string -> [ `Read ] t 
    val rw : string -> [ `Read | `Write ] t 
end 

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

module Container : sig 
    type 'a t = 
    {  
    owner: string; 
    socket: 'a Socket.t; 
    }  
end 

Answer 1

В общем, вы можете использовать экзистенциальные типы, чтобы забыть о каком-то параметре типа: вместо типа 'a foo, вы используете exists_foo, который содержит значение типа 'a foo для некоторого 'a вы не знаете. Существует несколько способов создания экзистенциальных типов в OCaml (полиморфные записи или первоклассные модули).

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

type untyped 

module Socket : sig 
    type 'a t 

    val ro : string -> [ `Read ] t 
    val rw : string -> [ `Read | `Write ] t 
    val untyped : 'a t -> untyped t 
end = struct 
    type 'a t = string 
    let ro s = s 
    let rw s = s 
    let untyped s = s 
end 

type t = { owner : string; socket : untyped Socket.t } 

let test = { 
    owner = "foo"; 
    socket = Socket.(untyped (ro "bar")) 
} 

Конечно, вы должны выбрать то, что возможно для нетипизированной розетки, для которого вы не знаете больше, как это было открыто. Может, это не то, что вы имели в виду?

Вы также можете держать гнездо в типе суммы, чтобы сохранить знания о его возможностях:

module Socket : sig 
    type 'a t 
    val ro : string -> [ `Read ] t 
    val rw : string -> [ `Read | `Write ] t 

    val read : [> `Read ] t -> unit 
    val write : [> `Write ] t -> unit 
end = struct 
    type 'a t = string 
    let ro s = s 
    let rw s = s 
    let read _ =() 
    let write _ =() 
end 

type some_socket = 
    | Ro of [ `Read ] Socket.t 
    | Rw of [ `Read | `Write ] Socket.t 

type t = { owner : string; socket : some_socket } 

let test = { 
    owner = "foo"; 
    socket = Ro (Socket.ro "bar") 
} 

let write container = match container.socket with 
    | Ro _ -> failwith "write not allowed" 
    | Rw s -> Socket.write s 

Наконец, есть еще один способ реализовать первое решение: вместо использования верхнего untyped типа, вы можете разрешить подтипирование значений в типе Socket. Для этого вам нужно указать в вашем интерфейсе дисперсию типа Socket.t: является ли он инвариантным ('a t), ковариантным (+'a t) или контравариантным (-'a t)?

Если ваша ментальная модель заключается в том, что тип фантомного варианта с большим количеством случаев является «более способным», тогда подтипирование должно идти от варианта с некоторыми случаями к варианту с меньшим количеством случаев, который является меньшим типом: иметь a t ≤ b t следует иметь a ≥ b (a имеет больше случаев): t должен быть контравариантным.

module Socket : sig 
    type -'a t 
    val ro : string -> [ `Read ] t 
    val rw : string -> [ `Read | `Write ] t 

    val read : [> `Read ] t -> unit 
    val write : [> `Write ] t -> unit 
end = struct 
    type 'a t = string 
    let ro s = s 
    let rw s = s 
    let read _ =() 
    let write _ =() 
end 

type t = { owner : string; socket : [ `Read ] Socket.t } 

let test = { 
    owner = "foo"; 
    socket = (Socket.rw "bar" :> [ `Read ] Socket.t) 
} 

Обратите внимание на явное приведение (socket :> [ `Read ]) Socket.t к меньшему типу сокета.