[Caml-list] Constrained existential types

[Caml-list] Constrained existential types

[Romain Bardou]

(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,

-- 
Romain Bardou

Re: [Caml-list] Constrained existential types

[Leo P White]

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,
>
>

Re: [Caml-list] Constrained existential types

[Romain Bardou]

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,
>>
>>
>
>

Re: [Caml-list] Constrained existential types

[Jacques Garrigue]

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