[Caml-list] Cyclic type abbreviation

[Caml-list] Cyclic type abbreviation

[Christoph Höger]

Dear all,

why is this type cyclic?

type node = int * tree * tree
 and tree = node option

I cannot introduce a manifest for the option type, as there is no Option
module (why is that, btw?) - so I would assume option to be special
enough to be handled like any other algebraic data type.
-- 
Christoph Höger

Technische Universität Berlin
Fakultät IV - Elektrotechnik und Informatik
Übersetzerbau und Programmiersprachen

Sekr. TEL12-2, Ernst-Reuter-Platz 7, 10587 Berlin

Tel.: +49 (30) 314-24890
E-Mail: christoph.hoeger@tu-berlin.de

Re: [Caml-list] Cyclic type abbreviation

[Mr. Herr]

On 13.11.2015 13:49, Christoph Höger wrote:
> Dear all,
>
> why is this type cyclic?
>
> type node = int * tree * tree
>  and tree = node option
>
> I cannot introduce a manifest for the option type, as there is no Option
> module (why is that, btw?) - so I would assume option to be special
> enough to be handled like any other algebraic data type.
type 'a option = None | Some 'a

no need for a module, just a simple type. Maybe you confound it with other languages.

And cyclic - well, the types are referring to each other.

Summary: what is supposedly wrong with it?

/Str.

RE: [Caml-list] Cyclic type abbreviation

[David Allsopp]

Mr. Herr wrote:
> On 13.11.2015 13:49, Christoph Höger wrote:
> > Dear all,
> >
> > why is this type cyclic?
> >
> > type node = int * tree * tree
> >  and tree = node option
> >
> > I cannot introduce a manifest for the option type, as there is no
> > Option module (why is that, btw?) - so I would assume option to be
> > special enough to be handled like any other algebraic data type.
> type 'a option = None | Some 'a
> 
> no need for a module, just a simple type. Maybe you confound it with other
> languages.
> 
> And cyclic - well, the types are referring to each other.
> 
> Summary: what is supposedly wrong with it?

I expect that what is wrong is that you can write:

type node = int * tree * tree
 and tree = Some of node
          | None

I don't know why you can't write [and tree = node option] instead.


David 

Re: [Caml-list] Cyclic type abbreviation

[Romain Bardou]

On 13/11/2015 14:37, David Allsopp wrote:
> Mr. Herr wrote:
>> On 13.11.2015 13:49, Christoph Höger wrote:
>>> Dear all,
>>>
>>> why is this type cyclic?
>>>
>>> type node = int * tree * tree
>>>   and tree = node option
>>>
>>> I cannot introduce a manifest for the option type, as there is no
>>> Option module (why is that, btw?) - so I would assume option to be
>>> special enough to be handled like any other algebraic data type.
>> type 'a option = None | Some 'a
>>
>> no need for a module, just a simple type. Maybe you confound it with other
>> languages.
>>
>> And cyclic - well, the types are referring to each other.
>>
>> Summary: what is supposedly wrong with it?
>
> I expect that what is wrong is that you can write:
>
> type node = int * tree * tree
>   and tree = Some of node
>            | None
>
> I don't know why you can't write [and tree = node option] instead.
>
>
> David
>

Interestingly, this definition is accepted:

type tree = (int * 'a * 'a) option as 'a

Here you are helping the type-checker because you give it a "canonical" 
representation that it can use when unifying; it no longer has to expand 
the type, potentially infinitely. I think the main point is that the 
type is isorecursive, but I'm not really an expert on the subject.

-- 
Romain Bardou

Re: [Caml-list] Cyclic type abbreviation

[Christoph Höger]

Am 13.11.2015 um 14:37 schrieb David Allsopp:
>> Summary: what is supposedly wrong with it?
> 
> I expect that what is wrong is that you can write:
> 
> type node = int * tree * tree
>  and tree = Some of node
>           | None
> 
> I don't know why you can't write [and tree = node option] instead.

Exactly, I do not understand why the builtin type option is handled
differently from a self-defined algebraic data type. I have a vague
understanding that the acyclic-property is sufficient for termination of
some operations on recursive types, but I wonder if option is just
missing a definition in the stdlib (so I could write a manifest, if that
would solve the issue) or if it is really something special.

-- 
Christoph Höger

Technische Universität Berlin
Fakultät IV - Elektrotechnik und Informatik
Übersetzerbau und Programmiersprachen

Sekr. TEL12-2, Ernst-Reuter-Platz 7, 10587 Berlin

Tel.: +49 (30) 314-24890
E-Mail: christoph.hoeger@tu-berlin.de

Re: [Caml-list] Cyclic type abbreviation

[Mr. Herr]

On 13.11.2015 14:37, David Allsopp wrote:
> Mr. Herr wrote:
>> On 13.11.2015 13:49, Christoph Höger wrote:
>>> Dear all,
>>>
>>> why is this type cyclic?
>>>
>>> type node = int * tree * tree
>>>  and tree = node option
>>>
>>> I cannot introduce a manifest for the option type, as there is no
>>> Option module (why is that, btw?) - so I would assume option to be
>>> special enough to be handled like any other algebraic data type.
>> type 'a option = None | Some 'a
>>
>> no need for a module, just a simple type. Maybe you confound it with other
>> languages.
>>
>> And cyclic - well, the types are referring to each other.
>>
>> Summary: what is supposedly wrong with it?
> I expect that what is wrong is that you can write:
>
> type node = int * tree * tree
>  and tree = Some of node
>           | None
>
> I don't know why you can't write [and tree = node option] instead.
>
>
>
Ah, did not see the problem at first sight...

Maybe that is why people so often define their own empty element:

# type node = Emptynode | Node of (int * node * node) ;;
type node = Emptynode | Node of (int * node * node)

# type node = Emptynode | Node of int * node * node ;; (* just had this parens
discussion... *)
type node = Emptynode | Node of int * node * node


/Str.

Re: [Caml-list] Cyclic type abbreviation

[Romain Bardou]

On 13/11/2015 14:46, Romain Bardou wrote:
> On 13/11/2015 14:37, David Allsopp wrote:
>> Mr. Herr wrote:
>>> On 13.11.2015 13:49, Christoph Höger wrote:
>>>> Dear all,
>>>>
>>>> why is this type cyclic?
>>>>
>>>> type node = int * tree * tree
>>>>   and tree = node option
>>>>
>>>> I cannot introduce a manifest for the option type, as there is no
>>>> Option module (why is that, btw?) - so I would assume option to be
>>>> special enough to be handled like any other algebraic data type.
>>> type 'a option = None | Some 'a
>>>
>>> no need for a module, just a simple type. Maybe you confound it with
>>> other
>>> languages.
>>>
>>> And cyclic - well, the types are referring to each other.
>>>
>>> Summary: what is supposedly wrong with it?
>>
>> I expect that what is wrong is that you can write:
>>
>> type node = int * tree * tree
>>   and tree = Some of node
>>            | None
>>
>> I don't know why you can't write [and tree = node option] instead.
>>
>>
>> David
>>
>
> Interestingly, this definition is accepted:
>
> type tree = (int * 'a * 'a) option as 'a
>
> Here you are helping the type-checker because you give it a "canonical"
> representation that it can use when unifying; it no longer has to expand
> the type, potentially infinitely. I think the main point is that the
> type is isorecursive, but I'm not really an expert on the subject.
>

My bad, I had actually redefined the option type as a polymorphic 
variant before:

type 'a option = [ `None | `Some of 'a ]

and I forgot about it when I tested the definition of tree above.

So yeah you can do that with polymorphic variants even though they are 
kind of type abbreviations.

Thanks to Daniel for pointing this out.

-- 
Romain

Re: [Caml-list] Cyclic type abbreviation

[Ben Millwood]

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

To be clear, options aren't being handled differently from any other
*pre-existing* user-defined type.

utop # type 'a my_type = One of 'a | Two of 'a * 'a;;
type 'a my_type = One of 'a | Two of 'a * 'a
utop # type node = int * tree * tree and tree = node my_type;;
Error: The type abbreviation node is cyclic

Using a real ADT instead of a type abbrevation works. David Allsopp already
gave one way you can do it, here is another which preserves the use of the
option type:

utop # type node = Node of int * tree * tree and tree = node option;;
type node = Node of int * tree * tree
and tree = node option

Note that here [tree] is still a type abbreviation, but [node] is not, so
the cycle is not a problem.

Note also that your original example works fine with the -rectypes flag.
But my general opinion is that if you need -rectypes to compile your code,
you should write different code :)

On 13 November 2015 at 22:24, Romain Bardou <romain@cryptosense.com> wrote:

> On 13/11/2015 14:46, Romain Bardou wrote:
>
>> On 13/11/2015 14:37, David Allsopp wrote:
>>
>>> Mr. Herr wrote:
>>>
>>>> On 13.11.2015 13:49, Christoph Höger wrote:
>>>>
>>>>> Dear all,
>>>>>
>>>>> why is this type cyclic?
>>>>>
>>>>> type node = int * tree * tree
>>>>>   and tree = node option
>>>>>
>>>>> I cannot introduce a manifest for the option type, as there is no
>>>>> Option module (why is that, btw?) - so I would assume option to be
>>>>> special enough to be handled like any other algebraic data type.
>>>>>
>>>> type 'a option = None | Some 'a
>>>>
>>>> no need for a module, just a simple type. Maybe you confound it with
>>>> other
>>>> languages.
>>>>
>>>> And cyclic - well, the types are referring to each other.
>>>>
>>>> Summary: what is supposedly wrong with it?
>>>>
>>>
>>> I expect that what is wrong is that you can write:
>>>
>>> type node = int * tree * tree
>>>   and tree = Some of node
>>>            | None
>>>
>>> I don't know why you can't write [and tree = node option] instead.
>>>
>>>
>>> David
>>>
>>>
>> Interestingly, this definition is accepted:
>>
>> type tree = (int * 'a * 'a) option as 'a
>>
>> Here you are helping the type-checker because you give it a "canonical"
>> representation that it can use when unifying; it no longer has to expand
>> the type, potentially infinitely. I think the main point is that the
>> type is isorecursive, but I'm not really an expert on the subject.
>>
>>
> My bad, I had actually redefined the option type as a polymorphic variant
> before:
>
> type 'a option = [ `None | `Some of 'a ]
>
> and I forgot about it when I tested the definition of tree above.
>
> So yeah you can do that with polymorphic variants even though they are
> kind of type abbreviations.
>
> Thanks to Daniel for pointing this out.
>
> --
> Romain
>
>
> --
> 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: 4573 bytes --]

Re: [Caml-list] Cyclic type abbreviation

[peterfrey]

Interestingly, this definition is accepted:
>
> type tree = (int * 'a * 'a) option as 'a
>
> Here you are helping the type-checker because you give it a 
> "canonical" representation that it can use when unifying; it no longer 
> has to expand the type, potentially infinitely. I think the main point 
> is that the type is isorecursive, but I'm not really an expert on the 
> subject.
>
with this type-checking business I sometimes have the feel being Alice 
in Wonderland; its getting curiouser and curiouser ...

The type : type node = int * tree * tree  and tree = node option is, in 
fact, accepted if you use the -rectypes option.
I just checked it with utop -rectypes

I wonder if this is considered bad (dangerous) style; but there are 
several things that would not work for me without this option.

Peter Frey

Re: [Caml-list] Cyclic type abbreviation

[Pierrick Couderc]

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

Actually, the "type recursivity" is syntactic: if you wrap your recursive
type in a data constructor or a record, there is no cycle in the type.
Using directly 'node option' won't work since syntactically there is no
data constructor to the unfold the type.
We know that the option type is an ADT so we can think that this definition
is correct and does not need the -rectypes flag, but the typechecker will
not infer such a characteristic and decide that, by looking at the type
definition, it is recursive since there is no constructor to fold and
unfold the type.

The only problem by redefining an option type especially for this
definition is that it won't be compatible with the built-in option type.
An idea to overcome this problem would be to be able to use the type
redefinition :

type tree =...
and type node = tree option = Some of tree | None

However, I don't know if it would be possible/sound, and really necessary
without complexifying the language.
Le 16 nov. 2015 5:43 PM, "peterfrey" <pjfrey@sympatico.ca> a écrit :

> Interestingly, this definition is accepted:
>
>>
>> type tree = (int * 'a * 'a) option as 'a
>>
>> Here you are helping the type-checker because you give it a "canonical"
>> representation that it can use when unifying; it no longer has to expand
>> the type, potentially infinitely. I think the main point is that the type
>> is isorecursive, but I'm not really an expert on the subject.
>>
>> with this type-checking business I sometimes have the feel being Alice in
> Wonderland; its getting curiouser and curiouser ...
>
> The type : type node = int * tree * tree  and tree = node option is, in
> fact, accepted if you use the -rectypes option.
> I just checked it with utop -rectypes
>
> I wonder if this is considered bad (dangerous) style; but there are
> several things that would not work for me without this option.
>
> Peter Frey
>
> --
> 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: 2917 bytes --]