Re: [Caml-list] Constrained existential types

[Leo P White <lpw25@cam.ac.uk>]

It is a bit convoluted, but you can achieve this by using a GADT:

type 'a t constraint 'a = [< `A | `B ];;

module type SIG =
sig
   type a = private [< `A | `B ]
   val x: a t
end;;

type 'a aux = Aux: 'a t -> ([< `A | `B] as 'a) aux;;

let create y =
  let helper: type u. u aux -> unit =
    fun (Aux y) -> 
        let module M: SIG =
        struct
          type a = u
          let x = y
        end
        in
        ()
  in
    helper (Aux y)
;;
 
Regards,

Leo


On Oct 23 2012, Romain Bardou wrote:

>(This is the 4th time I send this e-mail because it does not seem to 
>work. I'm trying with another SMTP server.)
>
>Hello list,
>
>I'm trying to use first-class modules to have existential types. But my 
>existential type must be constrained. I have the following code:
>
>type 'a t constraint 'a = [< `A | `B ]
>
>module type SIG =
>sig
>   type a = private [< `A | `B ]
>   val x: a t
>end
>
>let create (type u) (y: u t) =
>   let module M: SIG =
>     struct
>       type a = u
>       let x = y
>     end
>   in
>   ()
>
>It does not compile, because of the following error:
>
>Error: This type u should be an instance of type [< `A | `B ]
>
>In the manual I did not see any way to constrain type u. If I write 
>something like this instead:
>
>let create (y: 'a t) =
>   let module M: SIG =
>     struct
>       type a = 'a
>       let x = y
>     end
>   in
>   ()
>
>Then the definition "type a = 'a" is not correct, because 'a is not bound.
>
>Is there any way to have constrained existential types?
>
>Thanks,
>
>