[Caml-list] selecting GADT parameter

[Caml-list] selecting GADT parameter

[Ashish Agarwal]

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

I have:

type _ t =
| Foo1 : 'a * int -> int t
| Foo2 : 'a * string -> 'a t

but I really want to merge these two cases. I want the return type to be
based on the second arg when the second arg is int, and be based on the
first arg otherwise. Any way to accomplish that?

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

Re: [Caml-list] selecting GADT parameter

[Carl Eastlund]

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

Perhaps like this?  (Caveat: I typed this straight into gmail, I haven't
tried to compile or run this code at all.)

type ('a, 'b, 'c) tag =
| Tag1 : ('a, int, int) tag
| Tag2 : ('a, string, 'a) tag

type 'a t =
| Foo : ('a, 'b, 'c) tag * 'a * 'b -> 'c t

On Fri, Jul 31, 2015 at 9:48 AM, Ashish Agarwal <agarwal1975@gmail.com>
wrote:

> I have:
>
> type _ t =
> | Foo1 : 'a * int -> int t
> | Foo2 : 'a * string -> 'a t
>
> but I really want to merge these two cases. I want the return type to be
> based on the second arg when the second arg is int, and be based on the
> first arg otherwise. Any way to accomplish that?
>
>


-- 
Carl Eastlund

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

Re: [Caml-list] selecting GADT parameter

[Ashish Agarwal]

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

You essentially still have 2 constructors, so this isn't quite what I'm
aiming for.


On Fri, Jul 31, 2015 at 9:57 AM, Carl Eastlund <ceastlund@janestreet.com>
wrote:

> Perhaps like this?  (Caveat: I typed this straight into gmail, I haven't
> tried to compile or run this code at all.)
>
> type ('a, 'b, 'c) tag =
> | Tag1 : ('a, int, int) tag
> | Tag2 : ('a, string, 'a) tag
>
> type 'a t =
> | Foo : ('a, 'b, 'c) tag * 'a * 'b -> 'c t
>
> On Fri, Jul 31, 2015 at 9:48 AM, Ashish Agarwal <agarwal1975@gmail.com>
> wrote:
>
>> I have:
>>
>> type _ t =
>> | Foo1 : 'a * int -> int t
>> | Foo2 : 'a * string -> 'a t
>>
>> but I really want to merge these two cases. I want the return type to be
>> based on the second arg when the second arg is int, and be based on the
>> first arg otherwise. Any way to accomplish that?
>>
>>
>
>
> --
> Carl Eastlund
>

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

Re: [Caml-list] selecting GADT parameter

[Lukasz Stafiniak]

On the face of it, this is not possible. There must be as many pattern
matching branches as there are reachable conditions in the formulation
of the type, because only a pattern matching branch introduces a
conditional (an implication) into reasoning about types. In
particular, you need to pattern match against Tag1 and Tag2 if you
don't want to treat the parameter of the type "t" as an abstract type.

On Fri, Jul 31, 2015 at 4:18 PM, Ashish Agarwal <agarwal1975@gmail.com> wrote:
> You essentially still have 2 constructors, so this isn't quite what I'm
> aiming for.
>
>
> On Fri, Jul 31, 2015 at 9:57 AM, Carl Eastlund <ceastlund@janestreet.com>
> wrote:
>>
>> Perhaps like this?  (Caveat: I typed this straight into gmail, I haven't
>> tried to compile or run this code at all.)
>>
>> type ('a, 'b, 'c) tag =
>> | Tag1 : ('a, int, int) tag
>> | Tag2 : ('a, string, 'a) tag
>>
>> type 'a t =
>> | Foo : ('a, 'b, 'c) tag * 'a * 'b -> 'c t

Re: [Caml-list] selecting GADT parameter

[Runhang Li]

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

Hi, 




I don’t think it is possible. 




Suppose you can use only one type constructor. What should be the type of function “fun a b -> Foo (a, b)”?


Kindly,




Runhang

On Fri, Jul 31, 2015 at 3:18 PM, Ashish Agarwal <agarwal1975@gmail.com>
wrote:

> You essentially still have 2 constructors, so this isn't quite what I'm
> aiming for.
> On Fri, Jul 31, 2015 at 9:57 AM, Carl Eastlund <ceastlund@janestreet.com>
> wrote:
>> Perhaps like this?  (Caveat: I typed this straight into gmail, I haven't
>> tried to compile or run this code at all.)
>>
>> type ('a, 'b, 'c) tag =
>> | Tag1 : ('a, int, int) tag
>> | Tag2 : ('a, string, 'a) tag
>>
>> type 'a t =
>> | Foo : ('a, 'b, 'c) tag * 'a * 'b -> 'c t
>>
>> On Fri, Jul 31, 2015 at 9:48 AM, Ashish Agarwal <agarwal1975@gmail.com>
>> wrote:
>>
>>> I have:
>>>
>>> type _ t =
>>> | Foo1 : 'a * int -> int t
>>> | Foo2 : 'a * string -> 'a t
>>>
>>> but I really want to merge these two cases. I want the return type to be
>>> based on the second arg when the second arg is int, and be based on the
>>> first arg otherwise. Any way to accomplish that?
>>>
>>>
>>
>>
>> --
>> Carl Eastlund
>>
> -- 
> 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: 2510 bytes --]

Re: [Caml-list] selecting GADT parameter

[Goswin von Brederlow]

On Fri, Jul 31, 2015 at 09:48:13AM -0400, Ashish Agarwal wrote:
> I have:
> 
> type _ t =
> | Foo1 : 'a * int -> int t
> | Foo2 : 'a * string -> 'a t
> 
> but I really want to merge these two cases. I want the return type to be
> based on the second arg when the second arg is int, and be based on the
> first arg otherwise. Any way to accomplish that?

Say you had (imaginary syntax):

type _ t =
| Foo : 'a * int -> int t
| Foo : 'a * string -> 'a t

let x1 = Foo (1, 1)     : int t
let x2 = Foo (1, "x")   : int t

match (x : int t) with
| Foo (a, b) -> ...

What is the type of (a, b) now? Is it (int, int) or (int, string)?

MfG
	Goswin

Re: [Caml-list] selecting GADT parameter

[Ashish Agarwal]

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

Thanks for the answers. I see now the difficulty in this. (Though it seems
possible in theory if we required type annotations in various places.)

On Tue, Aug 4, 2015 at 5:21 AM, Goswin von Brederlow <goswin-v-b@web.de>
wrote:

> On Fri, Jul 31, 2015 at 09:48:13AM -0400, Ashish Agarwal wrote:
> > I have:
> >
> > type _ t =
> > | Foo1 : 'a * int -> int t
> > | Foo2 : 'a * string -> 'a t
> >
> > but I really want to merge these two cases. I want the return type to be
> > based on the second arg when the second arg is int, and be based on the
> > first arg otherwise. Any way to accomplish that?
>
> Say you had (imaginary syntax):
>
> type _ t =
> | Foo : 'a * int -> int t
> | Foo : 'a * string -> 'a t
>
> let x1 = Foo (1, 1)     : int t
> let x2 = Foo (1, "x")   : int t
>
> match (x : int t) with
> | Foo (a, b) -> ...
>
> What is the type of (a, b) now? Is it (int, int) or (int, string)?
>
> MfG
>         Goswin
>
> --
> 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: 2013 bytes --]