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

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

[Serge Sivkov]

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

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", 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

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

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

[Ivan Gotovchits]

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

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> 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", 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
>

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

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

[Mikhail Mandrykin]

[-- 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 --]