From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 E30BBE0128 for ; Tue, 30 Aug 2022 13:12:24 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=xavier.leroy@college-de-france.fr; spf=Pass smtp.mailfrom=xavier.leroy@college-de-france.fr; spf=None smtp.helo=postmaster@smtpout02-ext4.partage.renater.fr Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of xavier.leroy@college-de-france.fr) identity=pra; client-ip=194.254.241.31; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="xavier.leroy@college-de-france.fr"; x-sender="xavier.leroy@college-de-france.fr"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of xavier.leroy@college-de-france.fr designates 194.254.241.31 as permitted sender) identity=mailfrom; client-ip=194.254.241.31; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="xavier.leroy@college-de-france.fr"; x-sender="xavier.leroy@college-de-france.fr"; x-conformance=sidf_compatible; x-record-type="v=spf1"; x-record-text="v=spf1 a mx ip4:194.254.240.0/23 ip4:194.254.242.0/24 ip4:194.254.243.0/28 ~all" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@smtpout02-ext4.partage.renater.fr) identity=helo; client-ip=194.254.241.31; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="xavier.leroy@college-de-france.fr"; x-sender="postmaster@smtpout02-ext4.partage.renater.fr"; x-conformance=sidf_compatible IronPort-SDR: wnTABrkIbPyxW5D+kDJIBFGE3Soj+40tXwEu8hA6tmbq7o94JZORTji0Z5AV1FZLvCerIwBof3 LAa0ctSlKTIiFlHhqFYehENebr5M7DvbU/elF9CRmpElxcXeQS8Y5vPPJNdTuiNQfFIgmwUYa9 IECdJjXWFoWl2pGafgBrg2p7b3hyzuIwsegk9q1tJqjmQqWlNmzQI6r7f0yBYzYaHZHmKAZwnf x6dfLrG3MLa6TBPgLmBVip+ZEvuflFAIt+6UPucHw3HDWNy6/WLjkWkh3qz3S00B4nVBcQAajI rqRSeC88v50eDXK9FBI6AkFi X-IronPort-AV: E=Sophos;i="5.93,274,1654552800"; d="scan'208,217";a="50507969" X-MGA-submission: =?us-ascii?q?MDE8nKOUVdiT9iaJYDxebQMlF1ZXI8RpokH97H?= =?us-ascii?q?mK0Jd467nbpQN9hHqSj5v0VUQ8DiK6AK2ZBh8j4RSneq+ND0bm7oK5YI?= =?us-ascii?q?Msix2q9snYHUhJGaGpqfDWnBlFJqvql48QdAOrNtM8fcIz6VhH4oUf0H?= =?us-ascii?q?XWOnAjnG9zXQKAsLDmfyTMig=3D=3D?= Received: from smtpout02-ext4.partage.renater.fr ([194.254.241.31]) by mail2-smtp-roc.national.inria.fr with ESMTP; 30 Aug 2022 13:12:25 +0200 Received: from zmtaauth04.partage.renater.fr (zmtaauth04.partage.renater.fr [194.254.241.26]) by smtpout20.partage.renater.fr (Postfix) with ESMTP id 7D88CBFDA5 for ; Tue, 30 Aug 2022 13:12:23 +0200 (CEST) Received: from localhost (localhost [127.0.0.1]) by zmtaauth04.partage.renater.fr (Postfix) with ESMTP id 76E2E1C00BA for ; Tue, 30 Aug 2022 13:12:23 +0200 (CEST) Received: from zmtaauth04.partage.renater.fr ([127.0.0.1]) by localhost (zmtaauth04.partage.renater.fr [127.0.0.1]) (amavisd-new, port 10032) with ESMTP id 8Sp_BrqvF9j3 for ; Tue, 30 Aug 2022 13:12:23 +0200 (CEST) Received: from localhost (localhost [127.0.0.1]) by zmtaauth04.partage.renater.fr (Postfix) with ESMTP id 264781C00D7 for ; Tue, 30 Aug 2022 13:12:23 +0200 (CEST) DKIM-Filter: OpenDKIM Filter v2.10.3 zmtaauth04.partage.renater.fr 264781C00D7 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=college-de-france.fr; s=05BE819C-8883-4F62-9828-EF4D49272C46; t=1661857943; bh=+Uj0v32HJ3hNsdHVMzsjxKH/L2jR1OqVTA9R6G7FgC8=; h=MIME-Version:From:Date:Message-ID:To; b=VbsWhxotZi5W7D6kc4kX0xswW0riduoQXPqTSTkpRLBIcNnPWJs/ZFQL5cuCSmrlN 7t/k/tyxVfqXzUtpihV71+eldrAhJ8ipKFQaEuGEIReyD2eIeYtqrbxHh67VZi/JbK nSNpCWPvNEvBEJlnAOb0eun79FErzEy4EZ0iKRwALzhoaG39YZx1sun+RbmXglaMNw +VyFVhInw6rwQkZzxxPcKzEMW1MinYcs5CFt1kxJ5Ku7bJFnIlwPnm2h7Y3B/0jMnu 5xjCKZZG/d3luhhHVxFIcz/nnFkpkZe1/8Zti4C142OjG8T6v1lxSKH8ed4/5xcV1+ 0F5IDmQf9jqUg== X-Virus-Scanned: amavisd-new at zmtaauth04.partage.renater.fr Received: from zmtaauth04.partage.renater.fr ([127.0.0.1]) by localhost (zmtaauth04.partage.renater.fr [127.0.0.1]) (amavisd-new, port 10026) with ESMTP id V-WrVdqQ5Bbs for ; Tue, 30 Aug 2022 13:12:23 +0200 (CEST) Received: from 209.85.167.45 (unknown [194.254.241.249]) by zmtaauth04.partage.renater.fr (Postfix) with ESMTPA id EA6F01C00BA for ; Tue, 30 Aug 2022 13:12:22 +0200 (CEST) Received: by mail-lf1-f45.google.com with SMTP id j14so4694063lfu.4 for ; Tue, 30 Aug 2022 04:12:22 -0700 (PDT) X-Gm-Message-State: ACgBeo0htXdJsoGUYE+uZw+/rxSQUh2Pa+7c8RLZ5pSEknB4JLQp4The KE7soH3Jf9mqZ4fgnmT8x1CYe7VZ6i/s/1nHWEc= X-Google-Smtp-Source: AA6agR5U9mlbuTqBQ1eekaYoYIezj3lkr8NTZmQpa1sJYnowdcaHuccacTmNsoXy29KZLN6f7O+7ewXkejJYQp317YI= X-Received: by 2002:a05:6512:390f:b0:494:6c9a:bde0 with SMTP id a15-20020a056512390f00b004946c9abde0mr2529593lfu.344.1661857942466; Tue, 30 Aug 2022 04:12:22 -0700 (PDT) MIME-Version: 1.0 References: <25e68e2c-04d2-7764-e189-00812c08a34a@inria.fr> In-Reply-To: <25e68e2c-04d2-7764-e189-00812c08a34a@inria.fr> From: Xavier Leroy Date: Tue, 30 Aug 2022 13:11:55 +0200 X-Gmail-Original-Message-ID: Message-ID: To: Aaron Gray Cc: OCaML Mailing List Content-Type: multipart/alternative; boundary="00000000000053f77605e77374da" X-Renater-Ptge-SpamState: clean X-Renater-Ptge-SpamScore: -100 X-Renater-Ptge-SpamCause: gggruggvucftvghtrhhoucdtuddrgedvfedrvdekfedgfeekucetufdoteggodetrfdotffvucfrrhhofhhilhgvmecutffgpfetvffgtfenuceurghilhhouhhtmecufedttdenucesvcftvggtihhpihgvnhhtshculddquddttddmnecujfgurhepgghfjgfhfffkuffvvegtsegrtderredttdejnecuhfhrohhmpegirghvihgvrhcunfgvrhhohicuoeigrghvihgvrhdrlhgvrhhohiestgholhhlvghgvgdquggvqdhfrhgrnhgtvgdrfhhrqeenucggtffrrghtthgvrhhnpefhgeejhfevuddtveffvdelleelleevjeegffeggfdugfevffduiedtffejudegleenucffohhmrghinhepohgtrghmlhdrohhrghdpihhnrhhirgdrfhhrnecukfhppeduleegrddvheegrddvgedurddvgeelnecuvehluhhsthgvrhfuihiivgeptdenucfrrghrrghmpehinhgvthepudelgedrvdehgedrvdeguddrvdegledphhgvlhhopedvtdelrdekhedrudeijedrgeehpdhmrghilhhfrhhomhepiggrvhhivghrucfnvghrohihuceogigrvhhivghrrdhlvghrohihsegtohhllhgvghgvqdguvgdqfhhrrghntggvrdhfrheqpdhnsggprhgtphhtthhopedupdhrtghpthhtoheptggrmhhlqdhlihhsthesihhnrhhirgdrfhhr Subject: Re: [Caml-list] coinductive data types --00000000000053f77605e77374da Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Tue, Aug 30, 2022 at 9:24 AM Fran=C3=A7ois Pottier wrote: > > Hello, > > Le 29/08/2022 =C3=A0 17:43, Aaron Gray a =C3=A9crit : > > Does either ML or OCaML have coinductive data types ? And if so could > > you please point me at the/some appropriate documentation on them. > > ML and OCaml have algebraic data types, which are recursive (that is, > more general than inductive and co-inductive types). Algebraic data > type definitions are not subject to a positivity restriction, and > algebraic data types can be constructed and deconstructed by recursive > functions, which are not subject to a termination check. > > If you want to see a typical example of a "co-inductive" data structure > encoded in OCaml, I suggest to have a look at "sequences", which can be > described as potentially infinite lists: > > https://v2.ocaml.org/api/Seq.html > > Lazy evaluation (type Lazy.t) can also be used to define coinductive data structures. For concreteness, here are two definitions of the type of streams (infinite lists) : type 'a stream =3D unit -> 'a streamcell and 'a streamcell =3D { head: 'a; tail: 'a stream } type 'a stream =3D 'a streamcell Lazy.t and 'a streamcell =3D { head: 'a; t= ail: 'a stream } and of the stream of integers starting from n : let rec ints n =3D fun () -> { head =3D n; tail =3D ints (n + 1) } let rec ints n =3D lazy { head =3D n; tail =3D ints (n + 1) } Hope this helps, - Xavier Leroy > -- > Fran=C3=A7ois Pottier > francois.pottier@inria.fr > http://cambium.inria.fr/~fpottier/ > --00000000000053f77605e77374da Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On Tue, Aug 30, 2022 at 9:24 AM Fran=C3=A7ois Pottier <francois.pottier@inria.fr> wrote:=

Hello,

Le 29/08/2022 =C3=A0 17:43, Aaron Gray a =C3=A9crit=C2=A0:
> Does either ML or OCaML have coinductive data types ? And if so could<= br> > you please point me at the/some appropriate documentation on them.

ML and OCaml have algebraic data types, which are recursive (that is,
more general than inductive and co-inductive types). Algebraic data
type definitions are not subject to a positivity restriction, and
algebraic data types can be constructed and deconstructed by recursive
functions, which are not subject to a termination check.

If you want to see a typical example of a "co-inductive" data str= ucture
encoded in OCaml, I suggest to have a look at "sequences", which = can be
described as potentially infinite lists:

=C2=A0 =C2=A0https://v2.ocaml.org/api/Seq.html

Lazy evaluation (type Lazy.t) can also be used to def= ine coinductive data structures.

For concreteness,= here are two definitions of the type of streams (infinite lists) :

type 'a stream =3D unit -> 'a streamcell a= nd 'a streamcell =3D { head: 'a; tail: 'a stream }
ty= pe 'a stream =3D 'a streamcell Lazy.t and 'a streamcell =3D { h= ead: 'a; tail: 'a stream }
and of the stream of integers starting f= rom n :

let rec ints n =3D fun () -> { head =3D n; tail =3D ints (n + 1) }=
let rec ints n =3D lazy { head =3D n; tail= =3D ints (n + 1) }

Hope this helps,

- Xavier Leroy

=C2=A0
--
Fran=C3=A7ois Pottier
francois.pot= tier@inria.fr
http://cambium.inria.fr/~fpottier/
--00000000000053f77605e77374da--