[Caml-list] GADT definition

[Caml-list] GADT definition

[Lukasz Stafiniak]

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

Hi,

This is just a test so I'm not much concerned, but I have these definitions:

type z
type _ s
type (_, _, _) balance =
  | Less : (*∀'a.*) ('a, 'a s, 'a s) balance
  | Same : (*∀'b.*) ('b, 'b, 'b) balance
  | More : (*∀'a.*) ('a s, 'a, 'a s) balance
type _ aVL =
  | Leaf : z aVL
  | Node : (*∀'a, 'b, 'c.*)('a, 'b, 'c) balance * 'a aVL * int * 'b aVL ->
    ('c s) aVL

and I get the error for "type _ aVL =":

Error: In this definition, a type variable cannot be deduced
       from the type parameters.

What to do?

Regards,
Łukasz "lukstafi"

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

Re: [Caml-list] GADT definition

[Lukasz Stafiniak]

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

Sorry! I've spotted it reading the email. (I should read before sending.)


On Thu, Dec 19, 2013 at 11:17 PM, Lukasz Stafiniak <lukstafi@gmail.com>wrote:

> Hi,
>
> This is just a test so I'm not much concerned, but I have these
> definitions:
>
> type z
> type _ s
> type (_, _, _) balance =
>   | Less : (*∀'a.*) ('a, 'a s, 'a s) balance
>   | Same : (*∀'b.*) ('b, 'b, 'b) balance
>   | More : (*∀'a.*) ('a s, 'a, 'a s) balance
> type _ aVL =
>   | Leaf : z aVL
>
(here)

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

Re: [Caml-list] GADT definition

[Lukasz Stafiniak]

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

On Thu, Dec 19, 2013 at 11:20 PM, Lukasz Stafiniak <lukstafi@gmail.com>wrote:

> Sorry! I've spotted it reading the email. (I should read before sending.)
>
> No, that's not it. My question is still open.

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

Re: [Caml-list] GADT definition

[Milan Stanojević]

What version of ocaml are you using? It works for me on 4.00.1

On Thu, Dec 19, 2013 at 5:21 PM, Lukasz Stafiniak <lukstafi@gmail.com> wrote:
> On Thu, Dec 19, 2013 at 11:20 PM, Lukasz Stafiniak <lukstafi@gmail.com>
> wrote:
>>
>> Sorry! I've spotted it reading the email. (I should read before sending.)
>>
> No, that's not it. My question is still open.

Re: [Caml-list] GADT definition

[Lukasz Stafiniak]

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

On Thu, Dec 19, 2013 at 11:27 PM, Milan Stanojević <milanst@gmail.com>wrote:

> What version of ocaml are you using? It works for me on 4.00.1
>
>  OCaml 4.01.0 from OPAM.

 On Thu, Dec 19, 2013 at 5:21 PM, Lukasz Stafiniak <lukstafi@gmail.com>
> wrote:
> > On Thu, Dec 19, 2013 at 11:20 PM, Lukasz Stafiniak <lukstafi@gmail.com>
> > wrote:
> >>
> >> Sorry! I've spotted it reading the email. (I should read before
> sending.)
> >>
> > No, that's not it. My question is still open.
>

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

Re: [Caml-list] GADT definition

[Gabriel Scherer]

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

type z
type _ s

Don't use this kind of abstract type definition. Use instead (and export)
concrete definitions (even if you don't use their constructors for anything)

type 'a s = S of 'a
(or just type 'a s = S)

They have "better" injectivity properties. We've mentioned in on the
mailing-list a couple of time, and it's also the "easy take-away lesson"
from Jacques Garrigue talk at the OCaml workshop in September.


On Thu, Dec 19, 2013 at 11:35 PM, Lukasz Stafiniak <lukstafi@gmail.com>wrote:

> On Thu, Dec 19, 2013 at 11:27 PM, Milan Stanojević <milanst@gmail.com>wrote:
>
>> What version of ocaml are you using? It works for me on 4.00.1
>>
>>  OCaml 4.01.0 from OPAM.
>
>  On Thu, Dec 19, 2013 at 5:21 PM, Lukasz Stafiniak <lukstafi@gmail.com>
>> wrote:
>> > On Thu, Dec 19, 2013 at 11:20 PM, Lukasz Stafiniak <lukstafi@gmail.com>
>> > wrote:
>> >>
>> >> Sorry! I've spotted it reading the email. (I should read before
>> sending.)
>> >>
>> > No, that's not it. My question is still open.
>>
>
>

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

Re: [Caml-list] GADT definition

[Jacques Le Normand]

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

or type _ s = S


On Thu, Dec 19, 2013 at 6:10 PM, Gabriel Scherer
<gabriel.scherer@gmail.com>wrote:

> type z
> type _ s
>
> Don't use this kind of abstract type definition. Use instead (and export)
> concrete definitions (even if you don't use their constructors for anything)
>
> type 'a s = S of 'a
> (or just type 'a s = S)
>
> They have "better" injectivity properties. We've mentioned in on the
> mailing-list a couple of time, and it's also the "easy take-away lesson"
> from Jacques Garrigue talk at the OCaml workshop in September.
>
>
> On Thu, Dec 19, 2013 at 11:35 PM, Lukasz Stafiniak <lukstafi@gmail.com>wrote:
>
>> On Thu, Dec 19, 2013 at 11:27 PM, Milan Stanojević <milanst@gmail.com>wrote:
>>
>>> What version of ocaml are you using? It works for me on 4.00.1
>>>
>>>  OCaml 4.01.0 from OPAM.
>>
>>  On Thu, Dec 19, 2013 at 5:21 PM, Lukasz Stafiniak <lukstafi@gmail.com>
>>> wrote:
>>> > On Thu, Dec 19, 2013 at 11:20 PM, Lukasz Stafiniak <lukstafi@gmail.com
>>> >
>>> > wrote:
>>> >>
>>> >> Sorry! I've spotted it reading the email. (I should read before
>>> sending.)
>>> >>
>>> > No, that's not it. My question is still open.
>>>
>>
>>
>

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