Re: [Caml-list] using module with types as record parameter

[Mikhail Mandrykin <mandrykin@ispras.ru>]

[-- Attachment #1: Type: text/plain, Size: 3748 bytes --]

It's also possible to parametrize over abstract types (though only those 
without type parameters) that occur in first-class module signature:

module type CmdIface = sig
         type message
         val cmd : message -> int
end

module type NetIface = sig
         type init
         val net : init -> init
end

module Cmd = struct
         type message = int
         let cmd v = v+1
end

module Net = struct
         type 'a init = { cvt: (module CmdIface with type message = 'a) }

         let net (init : int init) =
                 let cvt = init.cvt in
                 let (module R) = cvt in
                 R.cmd 1 (* line 22 with error *)
end

let i = { Net.cvt = (module Cmd) };;
Net.net i;;

Also there's another type error in the example since types of cmd in the 
Cmdline module type and Cmd module are incompatible (_ -> unit vs. _ -> 
int).

On 28.11.2017 21:09, Ivan Gotovchits wrote:
> Let me first explain what is wrong with your code.
>
> The message type in `Cmdlface` is defined as an abstract type with 
> only one operation `cmd : message -> unit`. The module `Cmd` provides 
> a possible implementation for this abstract type.
> The `R.cmd 1` expression tries to break the abstraction by assuming 
> that the `R` implementation is using the `int` type as an underlying 
> implementation. Imagine, what will happen if the `Net.cvt` field 
> contained another implementation,
> for example
>
>     module Cmd = struct
>       type message = string
>       let cmd = print_endline
>     end
>
>     let i = { Net.cvt = (module Cmd: CmdIface) }
>     Net.net i
>
> This will finally lead to a call `print_endline 1` if the type system 
> won't stop you before.
>
>
> The solution is either to uncover the abstractions and stick to `int` 
> as a concrete representation of the message abstraction or to extend 
> the message abstraction interface with functions that will allow you 
> to create the messages, e.g.,
>
>
>     module type CmdIface = sig
>        type message
>        val of_int : int -> message
>        val cmd : message -> unit
>     end
>
>
>
>
>
> On Tue, Nov 28, 2017 at 12:55 PM, Serge Sivkov <ssp.mryau@gmail.com 
> <mailto:ssp.mryau@gmail.com>> wrote:
>
>     Hello,
>
>     is there way to fix the following code:
>
>     module type CmdIface = sig
>             type message
>             val cmd : message -> unit
>     end
>
>     module type NetIface = sig
>             type init
>             val net : init -> init
>     end
>
>     module Cmd = struct
>             type message = int
>             let cmd v = v+1
>     end
>
>     module Net = struct
>             type init = { cvt: (module CmdIface) }
>
>             let net init =
>                     let cvt = init.cvt in
>                     let module R = (val cvt: CmdIface) in
>                     R.cmd 1 (* line 22 with error *)
>     end
>
>     let i = { Net.cvt = (module Cmd: CmdIface) }
>     Net.net i
>
>     I got error:
>     File "t.ml <http://t.ml>", line 22, characters 22-23:
>     Error: This expression has type int but an expression was expected
>     of type
>              R.message
>
>     In case I do not use types in function signature code works well:
>     module type I = sig val f : int -> int end;;
>     module M = struct
>     let f v = v+1
>     end;;
>     type t = {cvt: (module M); v: int};;
>     let module R = (val i.cvt: I) in R.f i.v;;
>     - : int = 1
>
>     WBR, ssp
>
>

-- 
Mikhail Mandrykin
Linux Verification Center, ISPRAS
web: http://linuxtesting.org
e-mail: mandrykin@ispras.ru


[-- Attachment #2: Type: text/html, Size: 8161 bytes --]