[Caml-list] Explicitely named type variable and type constraints.

[Caml-list] Explicitely named type variable and type constraints.

[Philippe Veber]

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

Hi,

I found myself defining a type that would both contain a module type and a
type constraint:

  module type Screen = sig
    type state
    type message
    val init : state
    [...]
   val emit : state -> message option
  end
  type 'a screen = (module Screen with type message = 'a) constraint 'a =
[> `quit]

That is supposed to express that screens emit messages, and that one of the
messages can be "quit". Now I've got some trouble when using the 'a screen
type in a function that unpack the module it contains:

  let f (screen : 'a screen) =
    let module Screen = (val *screen* : Screen) in
    match Screen.(emit init) with
      | Some `quit -> 1
      | _ -> 0

  ;;
Error: This expression has type
         ([> `quit ] as 'a) screen = (module Screen with type message = 'a)
       but an expression was expected of type (module Screen)

New attempt:

# let f (screen : 'a screen) =
    let module Screen = (val screen : Screen with type message = 'a) in
    match Screen.(emit init) with
      | Some `quit -> 1
      | _ -> 0

  ;;
Error: Unbound type parameter 'a

Though here I'm not sure the error is right. New attempt:


# let f (type s) (screen : s screen) =
    let module Screen = (val screen : Screen with type message = s) in
    match Screen.(emit init) with
      | Some `quit -> 1
      | _ -> 0

  ;;
Error: This type s should be an instance of type [> `quit ]

Which makes sense. So here is my question: is there a way to impose a
constraint on the "newtype" introduced in argument? Let me say that I'm
aware I should write this more simply. For instance in the module type
Screen, emit could have type state -> [`quit | `message of message]. So my
question is only a matter of curiosity. Still, I'd be happy to know :o).

Cheers,
  Philippe.

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

Re: [Caml-list] Explicitely named type variable and type constraints.

[Jacques Garrigue]

On 2012/03/21, at 16:48, Philippe Veber wrote:

> Hi,
> 
> I found myself defining a type that would both contain a module type and a type constraint:
> 
>   module type Screen = sig
>     type state
>     type message
>     val init : state
>     [...] 
>    val emit : state -> message option
>   end
>   type 'a screen = (module Screen with type message = 'a) constraint 'a = [> `quit]
> 
> That is supposed to express that screens emit messages, and that one of the messages can be "quit". Now I've got some trouble when using the 'a screen type in a function that unpack the module it contains:
> 
>   let f (screen : 'a screen) = 
>     let module Screen = (val screen : Screen) in
>     match Screen.(emit init) with
>       | Some `quit -> 1
>       | _ -> 0
>     
>   ;;
> Error: This expression has type
>          ([> `quit ] as 'a) screen = (module Screen with type message = 'a)
>        but an expression was expected of type (module Screen)

Indeed, this is clearly wrong: these two module types are not equivalent.

> New attempt:
> 
> # let f (screen : 'a screen) = 
>     let module Screen = (val screen : Screen with type message = 'a) in
>     match Screen.(emit init) with
>       | Some `quit -> 1
>       | _ -> 0
>   
>   ;;
> Error: Unbound type parameter 'a

Wrong again, as subtyping between module signatures does not
allow free type variables.

> Though here I'm not sure the error is right. New attempt:
> 
> 
> # let f (type s) (screen : s screen) = 
>     let module Screen = (val screen : Screen with type message = s) in
>     match Screen.(emit init) with
>       | Some `quit -> 1
>       | _ -> 0
>   
>   ;;
> Error: This type s should be an instance of type [> `quit ]
> 
> Which makes sense. So here is my question: is there a way to impose a constraint on the "newtype" introduced in argument? Let me say that I'm aware I should write this more simply. For instance in the module type Screen, emit could have type state -> [`quit | `message of message]. So my question is only a matter of curiosity. Still, I'd be happy to know :o).

No, currently there is no way to do that.
One can only create locally abstract types, not locally private types.
In theory I see no problem doing that, but with the current approach this would require new syntax,
and be rather heavy.

  let f (type s = private [> `quit]) (screen : s screen) = ...

And to be fully general, recursion between those types should be allowed too...

As a side note, writing
	type message = private [> unit]
makes the problem clearer.
And solves it in some cases:

module type Screen =
  sig
    type state
    type message = private [> `quit ]
    val init : state
    val emit : state -> message option
  end
# let f (module Screen : Screen) =
    match Screen.(emit init) with
    | Some `quit -> 1
    | _ -> 0
  ;;
val f : (module Screen) -> int = <fun>

(using 4.00, but you can also write with (val ...))

Jacques Garrigue

Re: [Caml-list] Explicitely named type variable and type constraints.

[Alan Schmitt]

On 21 mars 2012, at 09:21, Jacques Garrigue wrote:

> (using 4.00, but you can also write with (val …))

Nice teaser ;-)

Alan

Re: [Caml-list] Explicitely named type variable and type constraints.

[Thomas Braibant]

On Wed, Mar 21, 2012 at 9:54 AM, Alan Schmitt
<alan.schmitt@polytechnique.org> wrote:
> On 21 mars 2012, at 09:21, Jacques Garrigue wrote:
>
>> (using 4.00, but you can also write with (val …))
>
> Nice teaser ;-)
>

Indeed, this is the second time I see an OCaml 4.00 mentionned (once
here, and once on the OCamlPro webpage, with an ETA ;)).

Is it the same future version of OCaml as the former 3.13, or is it
something different ?

Thomas

Re: [Caml-list] Explicitely named type variable and type constraints.

[Alain Frisch]

On 03/21/2012 10:01 AM, Thomas Braibant wrote:
> On Wed, Mar 21, 2012 at 9:54 AM, Alan Schmitt
> <alan.schmitt@polytechnique.org>  wrote:
>> On 21 mars 2012, at 09:21, Jacques Garrigue wrote:
>>
>>> (using 4.00, but you can also write with (val …))
>>
>> Nice teaser ;-)
>>
>
> Indeed, this is the second time I see an OCaml 4.00 mentionned (once
> here, and once on the OCamlPro webpage, with an ETA ;)).
>
> Is it the same future version of OCaml as the former 3.13, or is it
> something different ?

There is no mystery here. From 
http://caml.inria.fr/cgi-bin/viewvc.cgi/ocaml/version/ you can see that:

  - The 3.12 branch has been closed.
  - A new 4.00 branch has been created.


-- Alain

Re: [Caml-list] Explicitely named type variable and type constraints.

[Philippe Veber]

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

Thanks for your answer Jacques!

>          ([> `quit ] as 'a) screen = (module Screen with type message =
> 'a)
> >        but an expression was expected of type (module Screen)
>
> Indeed, this is clearly wrong: these two module types are not equivalent.
>
Right, that one was obvious.


> > New attempt:
> >
> > # let f (screen : 'a screen) =
> >     let module Screen = (val screen : Screen with type message = 'a) in
> >     match Screen.(emit init) with
> >       | Some `quit -> 1
> >       | _ -> 0
> >
> >   ;;
> > Error: Unbound type parameter 'a
>
> Wrong again, as subtyping between module signatures does not
> allow free type variables.
>
At some point, I remember having a message saying that indeed type
variables are not allowed while unpacking the module, at least something
closer to what you say and more specific than "unbound type parameter 'a".
So I'd say it would be more convenient to have a specific message (just
like there is for unbound type variables in class definitions for
instance). If you don't consider it too futile, I can test it on the SVN
head and file a bug report if appropriate.


>
> > Though here I'm not sure the error is right. New attempt:
> >
> >
> > # let f (type s) (screen : s screen) =
> >     let module Screen = (val screen : Screen with type message = s) in
> >     match Screen.(emit init) with
> >       | Some `quit -> 1
> >       | _ -> 0
> >
> >   ;;
> > Error: This type s should be an instance of type [> `quit ]
> >
> > Which makes sense. So here is my question: is there a way to impose a
> constraint on the "newtype" introduced in argument? Let me say that I'm
> aware I should write this more simply. For instance in the module type
> Screen, emit could have type state -> [`quit | `message of message]. So my
> question is only a matter of curiosity. Still, I'd be happy to know :o).
>
> No, currently there is no way to do that.
> One can only create locally abstract types, not locally private types.
>
Ok.


> In theory I see no problem doing that, but with the current approach this
> would require new syntax,
> and be rather heavy.
>
>  let f (type s = private [> `quit]) (screen : s screen) = ...
>
> And to be fully general, recursion between those types should be allowed
> too...
>
Probably not worth the trouble. I'm just not used to writing a type and not
being able to write a function using values of this type afterwards :o).


>
> As a side note, writing
>        type message = private [> unit]
> makes the problem clearer.
> And solves it in some cases:
>
> module type Screen =
>  sig
>    type state
>     type message = private [> `quit ]
>    val init : state
>     val emit : state -> message option
>  end
> # let f (module Screen : Screen) =
>     match Screen.(emit init) with
>    | Some `quit -> 1
>    | _ -> 0
>  ;;
> val f : (module Screen) -> int = <fun>
>
Indeed that works! (with appropriate 3.12 syntax).

# module type Screen
=

 sig

   type
state

   type message = private [> `quit
]

   val init :
state

   val emit : state -> message
option

 end;;

module type Screen
=


sig

    type
state

    type message = private [> `quit ]
    val init : state
    val emit : state -> message option
  end
# let f screen = let module Screen = (val screen : Screen) in match
Screen.emit Screen.init with Some `quit -> 1 | _ ->
0;;
val f : (module Screen) -> int =
<fun>

# module Screen1 : Screen = struct type state = unit type message = [`a |
`quit] let init = () let emit () = Some `a
end;;
module Screen1 :
Screen

# module Screen2 : Screen = struct type state = int type message = [`a |
`quit] let init = 0 let emit _ = Some `quit
end;;
module Screen2 :
Screen

# [ (module Screen1 : Screen) ; (module Screen2 : Screen)
];;

- : (module Screen) list = [<module>;
<module>]


This nearly solves my problem: there will be several Screen modules, and
those should share a common message type, so that they can communicate.
That's why I introduced the 'a screen type. However, it seems that I can't
define it anymore:

# type 'a screen = (module Screen with type message = 'a) constraint 'a =
[>
`quit];;

Error: In this `with' constraint, the new definition of
message

       does not match its original definition in the constrained
signature:

       Type declarations do not
match:

         type message
       is not included in
         type message = private [> `quit ]

# type 'a screen = (module Screen with type message = 'a constraint 'a = [>
`quit]);;

Error: Syntax
error


It's only logical the first attempt fails. The second, however, seems more
reasonable to me (but I guess if type constraints are only allowed in type
definition there must be a good reason). Is there a workaround? In the end,
I'd want to define a list of Screen modules that share a common message
type containing the `quit tag. That said, I remember the work by Romain
Bardou and yourself on unions of private polymorphic variants, and I guess
we might face difficult problems here. In any case, I have a backup
solution, so it's no big deal if it isn't possible.



> (using 4.00, but you can also write with (val ...))
>
> That remark was unfortunate: now my thread is spoiled for sure :o)))

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