Re: [Caml-list] Constrained existential types

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

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

2012/10/23 21:32 "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

This is very interesting.
I was actually convinced that this was impossible.
The problem is that the (type u) syntax does not support abstract rows.
But you could avoid it by using a gadt which restores this abstract row
after abstracting the whole type.

Actually the type u. u aux->unit is hard to understand here.
The point is that it expand to 'u. 'u aux->unit, which really requires a
polymorphic row variable.
Unfortunately the following implicit (type u) does not capture it buy your
gadt does the trick.

Jacques Garrigue

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

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