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

[Philippe Veber <philippe.veber@gmail.com>]

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