From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id DFE557EEFC for ; Mon, 16 Nov 2015 18:08:36 +0100 (CET) IronPort-PHdr: 9a23:4Jb/qB9J/Kjke/9uRHKM819IXTAuvvDOBiVQ1KB80OocTK2v8tzYMVDF4r011RmSDdidtq0P2rOempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXsq3G/pQQfBg/4fVIsYL+lR8iP0I/mjqibwN76XUZhvHKFe7R8LRG7/036l/I9ps9cEJs30QbDuXBSeu5blitCLFOXmAvgtI/rpMYwuwwZgf8q9tZBXKPmZOx4COUAVHV1BVso/9XmvgXvSg6G531UEjlH00kAPw+Q9BzmU43/qCbr/r5l2ieAMNzeVqExQT2+7qxsDhTh3mNPOzMn/WWUi8pqjatzpxmoohhn2YmSa4aQZ9RkeaaIRdIXX3BAVcUZfCtcDo6mZMNbF+sMJ/xZpIq7rFwToRakDiGrD+rqzidSgTn92qhsgLdpKh3PwAF1R4FGi3/TttigcfpLXA== Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierrick.couderc@ocamlpro.com; spf=None smtp.mailfrom=pierrick.couderc@ocamlpro.com; spf=None smtp.helo=postmaster@smtp4-g21.free.fr Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of pierrick.couderc@ocamlpro.com) identity=pra; client-ip=212.27.42.4; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="pierrick.couderc@ocamlpro.com"; x-sender="pierrick.couderc@ocamlpro.com"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of pierrick.couderc@ocamlpro.com) identity=mailfrom; client-ip=212.27.42.4; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="pierrick.couderc@ocamlpro.com"; x-sender="pierrick.couderc@ocamlpro.com"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@smtp4-g21.free.fr) identity=helo; client-ip=212.27.42.4; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="pierrick.couderc@ocamlpro.com"; x-sender="postmaster@smtp4-g21.free.fr"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0DPAACeDEpWnAQqG9RdhA5vAQWvCZFDIYVvAoE8BzwQAQEBAQEBAQEQAQEBAQEGDQkJIS6CLYIIAQEDARIRSAMLBQsLBAcaHQICIhIBBQEKEgYBEhIQh3cDCggECZxbgTE+MYtIizADhF0BAQEBAQEBAwEBAQEBAQEBAQEBGIZUhH6FCIJtgUQFhgsMkDGFHYgKgVtJli+CJRIkgRcRJ4JSgV5xhUsBAQE X-IPAS-Result: A0DPAACeDEpWnAQqG9RdhA5vAQWvCZFDIYVvAoE8BzwQAQEBAQEBAQEQAQEBAQEGDQkJIS6CLYIIAQEDARIRSAMLBQsLBAcaHQICIhIBBQEKEgYBEhIQh3cDCggECZxbgTE+MYtIizADhF0BAQEBAQEBAwEBAQEBAQEBAQEBGIZUhH6FCIJtgUQFhgsMkDGFHYgKgVtJli+CJRIkgRcRJ4JSgV5xhUsBAQE X-IronPort-AV: E=Sophos;i="5.20,303,1444687200"; d="scan'208";a="187751287" Received: from smtp4-g21.free.fr ([212.27.42.4]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/ADH-AES256-GCM-SHA384; 16 Nov 2015 18:08:36 +0100 Received: from mail-lb0-f179.google.com (unknown [209.85.217.179]) (Authenticated sender: pierrickcouderc) by smtp4-g21.free.fr (Postfix) with ESMTPSA id 32D374C80E3 for ; Mon, 16 Nov 2015 18:08:33 +0100 (CET) Received: by lbbsy6 with SMTP id sy6so63636128lbb.2 for ; Mon, 16 Nov 2015 09:08:35 -0800 (PST) MIME-Version: 1.0 X-Received: by 10.112.162.97 with SMTP id xz1mr4381972lbb.29.1447693715472; Mon, 16 Nov 2015 09:08:35 -0800 (PST) Received: by 10.112.55.39 with HTTP; Mon, 16 Nov 2015 09:08:35 -0800 (PST) Received: by 10.112.55.39 with HTTP; Mon, 16 Nov 2015 09:08:35 -0800 (PST) In-Reply-To: <564A078B.80309@sympatico.ca> References: <5645DC49.7050106@tu-berlin.de> <5645E255.5060900@freenet.de> <5645E9B4.9080007@cryptosense.com> <564A078B.80309@sympatico.ca> Date: Mon, 16 Nov 2015 18:08:35 +0100 X-Gmail-Original-Message-ID: Message-ID: From: Pierrick Couderc To: peterfrey , devel+inria@ocamlpro.com Cc: Ocaml Mailing List Content-Type: multipart/alternative; boundary=089e01160498a78bb30524ab75c4 X-Validation-by: pierrickcouderc@gmail.com Subject: Re: [Caml-list] Cyclic type abbreviation --089e01160498a78bb30524ab75c4 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable 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 =3D... and type node =3D tree option =3D 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" a =C3=A9crit : > Interestingly, this definition is accepted: > >> >> type tree =3D (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 =3D int * tree * tree and tree =3D 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 > --089e01160498a78bb30524ab75c4 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable

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 sin= ce 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 def= inition, it is recursive since there is no constructor to fold and unfold t= he type.

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

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

However, I don't know if it would be possible/sound, and= really necessary without complexifying the language.

Le=C2=A016 nov. 2015 5:43 PM, "peterfrey&qu= ot; <pjfrey@sympatico.ca> = a =C3=A9crit=C2=A0:
= Interestingly, this definition is accepted:

type tree =3D (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 ex= pand the type, potentially infinitely. I think the main point is that the t= ype 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 W= onderland; its getting curiouser and curiouser ...

The type : type node =3D int * tree * tree=C2=A0 and tree =3D node option i= s, 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.=C2=A0 Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocam= l_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs
--089e01160498a78bb30524ab75c4--