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
--
Caml-list mailing list. Subscription management and archives:
https://sympa-roc.inria.fr/wws/info/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs
