Re: [Caml-list] Constrained existential types

[Romain Bardou <romain.bardou@inria.fr>]

Interesting. I can't use OCaml 4.00 or more for this project (yet) but 
I'll keep that in mind.

Cheers,

-- 
Romain Bardou

Le 23/10/2012 14:31, Leo P White a écrit :
> 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,
>>
>>
>
>