[Caml-list] coinductive data types

[Caml-list] coinductive data types

[Aaron Gray]

Does either ML or OCaML have coinductive data types ? And if so could
you please point me at the/some appropriate documentation on them.

Many thanks in advance,

Aaron

Re: [Caml-list] coinductive data types

[François Pottier]

Hello,

Le 29/08/2022 à 17:43, Aaron Gray a écrit :
> 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

-- 
François Pottier
francois.pottier@inria.fr
http://cambium.inria.fr/~fpottier/

Re: [Caml-list] coinductive data types

[Xavier Leroy]

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

On Tue, Aug 30, 2022 at 9:24 AM François Pottier <francois.pottier@inria.fr>
wrote:

>
> Hello,
>
> Le 29/08/2022 à 17:43, Aaron Gray a écrit :
> > 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 = unit -> 'a streamcell and 'a streamcell = { head: 'a;
tail: 'a stream }
type 'a stream = 'a streamcell Lazy.t and 'a streamcell = { head: 'a; tail:
'a stream }

and of the stream of integers starting from n :

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

Hope this helps,

- Xavier Leroy



> --
> François Pottier
> francois.pottier@inria.fr
> http://cambium.inria.fr/~fpottier/
>

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

Re: [Caml-list] coinductive data types

[Aaron Gray]

On Tue, 30 Aug 2022 at 12:12, Xavier Leroy
<xavier.leroy@college-de-france.fr> wrote:
>
> On Tue, Aug 30, 2022 at 9:24 AM François Pottier <francois.pottier@inria.fr> wrote:
>>
>>
>> Hello,
>>
>> Le 29/08/2022 à 17:43, Aaron Gray a écrit :
>> > 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.

Hello Xavier,

Thanks for putting me straight on that.

My original path of inquiry which I should have actually stated was
regarding how to go about implementing subtyping of mutually recursive
algebraic data types.

I am looking on how to go about this and using coinduction and
bisimulation seemed like the best fit or correct way to go about this.

Does OCaML use/handle subtyping of mutually recursive algebraic data
types ? And if so, is its implementation easily accessible ?

>> 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 = unit -> 'a streamcell and 'a streamcell = { head: 'a; tail: 'a stream }
> type 'a stream = 'a streamcell Lazy.t and 'a streamcell = { head: 'a; tail: 'a stream }
>
> and of the stream of integers starting from n :
>
> let rec ints n = fun () -> { head = n; tail = ints (n + 1) }
> let rec ints n = lazy { head = n; tail = ints (n + 1) }

Thank you, yes I am familiar with this type of usage.

Regards,

Aaron

>>
>
> Hope this helps,
>
> - Xavier Leroy
>
>
>>
>> --
>> François Pottier
>> francois.pottier@inria.fr
>> http://cambium.inria.fr/~fpottier/



-- 
Aaron Gray

Independent Open Source Software Engineer, Computer Language
Researcher, Information Theorist, and amateur computer scientist.

Re: [Caml-list] coinductive data types

[Jacques Garrigue]

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

Hello Aaron,

If you are interested in the subtyping already available inside OCaml,
it provides width subtyping for both objects and polymorphic variants.
Polymorphic variants are algebraic datatypes, but their equality is
structural rather than nominal, and they are limited to regular type
definitions.

For instance, the following subtyping on two variants of potentially infinite
streams is available:

type 'a seq = 'a seqc lazy_t and 'a seqc = [`Nil | `Cons of 'a * 'a seq]
type 'a aseq = 'a aseqc lazy_t
 and 'a aseqc = ['a seqc | `App of 'a aseq * 'a aseq]
let sub x = (x : 'a seq :> 'a aseq)
(* val sub : 'a seq -> 'a aseq *)

Jacques Garrigue

> 2022/08/30 21:33、Aaron Gray <aaronngray.lists@gmail.com <mailto:aaronngray.lists@gmail.com>>のメール:
> 
> On Tue, 30 Aug 2022 at 12:12, Xavier Leroy
> <xavier.leroy@college-de-france.fr <mailto:xavier.leroy@college-de-france.fr>> wrote:
>> 
>> On Tue, Aug 30, 2022 at 9:24 AM François Pottier <francois.pottier@inria.fr <mailto:francois.pottier@inria.fr>> wrote:
>>> 
>>> 
>>> Hello,
>>> 
>>> Le 29/08/2022 à 17:43, Aaron Gray a écrit :
>>>> 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.
> 
> Hello Xavier,
> 
> Thanks for putting me straight on that.
> 
> My original path of inquiry which I should have actually stated was
> regarding how to go about implementing subtyping of mutually recursive
> algebraic data types.
> 
> I am looking on how to go about this and using coinduction and
> bisimulation seemed like the best fit or correct way to go about this.
> 
> Does OCaML use/handle subtyping of mutually recursive algebraic data
> types ? And if so, is its implementation easily accessible ?
> 
>>> 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 <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 = unit -> 'a streamcell and 'a streamcell = { head: 'a; tail: 'a stream }
>> type 'a stream = 'a streamcell Lazy.t and 'a streamcell = { head: 'a; tail: 'a stream }
>> 
>> and of the stream of integers starting from n :
>> 
>> let rec ints n = fun () -> { head = n; tail = ints (n + 1) }
>> let rec ints n = lazy { head = n; tail = ints (n + 1) }
> 
> Thank you, yes I am familiar with this type of usage.
> 
> Regards,
> 
> Aaron
> 
>>> 
>> 
>> Hope this helps,
>> 
>> - Xavier Leroy
>> 
>> 
>>> 
>>> --
>>> François Pottier
>>> francois.pottier@inria.fr <mailto:francois.pottier@inria.fr>
>>> http://cambium.inria.fr/~fpottier/
> 
> 
> 
> -- 
> Aaron Gray
> 
> Independent Open Source Software Engineer, Computer Language
> Researcher, Information Theorist, and amateur computer scientist.


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

Re: [Caml-list] coinductive data types

[Aaron Gray]

Jacques,

I will get a raw OCaML Docker image, and have a play with this.

What is going on there, does ':>' return a conversion function as well
as being 'true' and secondly a predicate ?

Thanks,

Aaron



On Wed, 31 Aug 2022 at 02:15, Jacques Garrigue
<jacques.garrigue@gmail.com> wrote:
>
> Hello Aaron,
>
> If you are interested in the subtyping already available inside OCaml,
> it provides width subtyping for both objects and polymorphic variants.
> Polymorphic variants are algebraic datatypes, but their equality is
> structural rather than nominal, and they are limited to regular type
> definitions.
>
> For instance, the following subtyping on two variants of potentially infinite
> streams is available:
>
> type 'a seq = 'a seqc lazy_t and 'a seqc = [`Nil | `Cons of 'a * 'a seq]
> type 'a aseq = 'a aseqc lazy_t
>  and 'a aseqc = ['a seqc | `App of 'a aseq * 'a aseq]
> let sub x = (x : 'a seq :> 'a aseq)
> (* val sub : 'a seq -> 'a aseq *)
>
> Jacques Garrigue
>
> 2022/08/30 21:33、Aaron Gray <aaronngray.lists@gmail.com>のメール:
>
> On Tue, 30 Aug 2022 at 12:12, Xavier Leroy
> <xavier.leroy@college-de-france.fr> wrote:
>
>
> On Tue, Aug 30, 2022 at 9:24 AM François Pottier <francois.pottier@inria.fr> wrote:
>
>
>
> Hello,
>
> Le 29/08/2022 à 17:43, Aaron Gray a écrit :
>
> 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.
>
>
> Hello Xavier,
>
> Thanks for putting me straight on that.
>
> My original path of inquiry which I should have actually stated was
> regarding how to go about implementing subtyping of mutually recursive
> algebraic data types.
>
> I am looking on how to go about this and using coinduction and
> bisimulation seemed like the best fit or correct way to go about this.
>
> Does OCaML use/handle subtyping of mutually recursive algebraic data
> types ? And if so, is its implementation easily accessible ?
>
> 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 = unit -> 'a streamcell and 'a streamcell = { head: 'a; tail: 'a stream }
> type 'a stream = 'a streamcell Lazy.t and 'a streamcell = { head: 'a; tail: 'a stream }
>
> and of the stream of integers starting from n :
>
> let rec ints n = fun () -> { head = n; tail = ints (n + 1) }
> let rec ints n = lazy { head = n; tail = ints (n + 1) }
>
>
> Thank you, yes I am familiar with this type of usage.
>
> Regards,
>
> Aaron
>
>
>
> Hope this helps,
>
> - Xavier Leroy
>
>
>
> --
> François Pottier
> francois.pottier@inria.fr
> http://cambium.inria.fr/~fpottier/
>
>
>
>
> --
> Aaron Gray
>
> Independent Open Source Software Engineer, Computer Language
> Researcher, Information Theorist, and amateur computer scientist.
>
>


-- 
Aaron Gray

Independent Open Source Software Engineer, Computer Language
Researcher, Information Theorist, and amateur computer scientist.

Re: [Caml-list] coinductive data types

[Jacques Garrigue]

Hi Aaron,

No, there is no physical coercion involved.
Polymorphic variants have a uniform representation of constructor tags
(through a hashing function) so that (`Cons(1, lazy `Nil)) has always the same
representation, be it as int seqc or int aseqc.
So we are just talking about the different types the same value can be given.

Jacques

> 2022/08/31 12:22、Aaron Gray <aaronngray.lists@gmail.com>のメール:
> 
> Jacques,
> 
> I will get a raw OCaML Docker image, and have a play with this.
> 
> What is going on there, does ':>' return a conversion function as well
> as being 'true' and secondly a predicate ?
> 
> Thanks,
> 
> Aaron
> 
> 
> 
> On Wed, 31 Aug 2022 at 02:15, Jacques Garrigue
> <jacques.garrigue@gmail.com> wrote:
>> 
>> Hello Aaron,
>> 
>> If you are interested in the subtyping already available inside OCaml,
>> it provides width subtyping for both objects and polymorphic variants.
>> Polymorphic variants are algebraic datatypes, but their equality is
>> structural rather than nominal, and they are limited to regular type
>> definitions.
>> 
>> For instance, the following subtyping on two variants of potentially infinite
>> streams is available:
>> 
>> type 'a seq = 'a seqc lazy_t and 'a seqc = [`Nil | `Cons of 'a * 'a seq]
>> type 'a aseq = 'a aseqc lazy_t
>> and 'a aseqc = ['a seqc | `App of 'a aseq * 'a aseq]
>> let sub x = (x : 'a seq :> 'a aseq)
>> (* val sub : 'a seq -> 'a aseq *)
>> 
>> Jacques Garrigue
>> 
>> 2022/08/30 21:33、Aaron Gray <aaronngray.lists@gmail.com>のメール:
>> 
>> On Tue, 30 Aug 2022 at 12:12, Xavier Leroy
>> <xavier.leroy@college-de-france.fr> wrote:
>> 
>> 
>> On Tue, Aug 30, 2022 at 9:24 AM François Pottier <francois.pottier@inria.fr> wrote:
>> 
>> 
>> 
>> Hello,
>> 
>> Le 29/08/2022 à 17:43, Aaron Gray a écrit :
>> 
>> 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.
>> 
>> 
>> Hello Xavier,
>> 
>> Thanks for putting me straight on that.
>> 
>> My original path of inquiry which I should have actually stated was
>> regarding how to go about implementing subtyping of mutually recursive
>> algebraic data types.
>> 
>> I am looking on how to go about this and using coinduction and
>> bisimulation seemed like the best fit or correct way to go about this.
>> 
>> Does OCaML use/handle subtyping of mutually recursive algebraic data
>> types ? And if so, is its implementation easily accessible ?
>> 
>> 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 = unit -> 'a streamcell and 'a streamcell = { head: 'a; tail: 'a stream }
>> type 'a stream = 'a streamcell Lazy.t and 'a streamcell = { head: 'a; tail: 'a stream }
>> 
>> and of the stream of integers starting from n :
>> 
>> let rec ints n = fun () -> { head = n; tail = ints (n + 1) }
>> let rec ints n = lazy { head = n; tail = ints (n + 1) }
>> 
>> 
>> Thank you, yes I am familiar with this type of usage.
>> 
>> Regards,
>> 
>> Aaron
>> 
>> 
>> 
>> Hope this helps,
>> 
>> - Xavier Leroy
>> 
>> 
>> 
>> --
>> François Pottier
>> francois.pottier@inria.fr
>> http://cambium.inria.fr/~fpottier/
>> 
>> 
>> 
>> 
>> --
>> Aaron Gray
>> 
>> Independent Open Source Software Engineer, Computer Language
>> Researcher, Information Theorist, and amateur computer scientist.
>> 
>> 
> 
> 
> -- 
> Aaron Gray
> 
> Independent Open Source Software Engineer, Computer Language
> Researcher, Information Theorist, and amateur computer scientist.

Re: [Caml-list] coinductive data types

[Aaron Gray]

Hello François,

Thanks for putting me straight on that.

My original path of inquiry which I should have actually stated was
regarding how to go about implementing subtyping of mutually recursive
algebraic data types.

I am looking on how to go about this and using coinduction and
bisimulation seemed like the best fit or correct way to go about this.

Does OCaML use/handle subtyping of mutually recursive algebraic data
types ? And if so, is its implementation easily accessible ?

Sorry I got you and Xavier muddled up somehow !

Regards,

Aaron

On Tue, 30 Aug 2022 at 08:24, François Pottier
<francois.pottier@inria.fr> wrote:
>
>
> Hello,
>
> Le 29/08/2022 à 17:43, Aaron Gray a écrit :
> > 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
>
> --
> François Pottier
> francois.pottier@inria.fr
> http://cambium.inria.fr/~fpottier/



-- 
Aaron Gray

Independent Open Source Software Engineer, Computer Language
Researcher, Information Theorist, and amateur computer scientist.

Re: [Caml-list] coinductive data types

[Nate Foster]

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

Hi Aaron,

You might be interested in looking at CoCaml. It was developed by
Jean-Baptiste Jeannin as part of his PhD, in collaboration with his advisor
Dexter Kozen and Alexandra Silva.

https://www.cs.cornell.edu/Projects/CoCaml/

Cheers,
-N

On Tue, Aug 30, 2022 at 8:38 AM Aaron Gray <aaronngray.lists@gmail.com>
wrote:

> Hello François,
>
> Thanks for putting me straight on that.
>
> My original path of inquiry which I should have actually stated was
> regarding how to go about implementing subtyping of mutually recursive
> algebraic data types.
>
> I am looking on how to go about this and using coinduction and
> bisimulation seemed like the best fit or correct way to go about this.
>
> Does OCaML use/handle subtyping of mutually recursive algebraic data
> types ? And if so, is its implementation easily accessible ?
>
> Sorry I got you and Xavier muddled up somehow !
>
> Regards,
>
> Aaron
>
> On Tue, 30 Aug 2022 at 08:24, François Pottier
> <francois.pottier@inria.fr> wrote:
> >
> >
> > Hello,
> >
> > Le 29/08/2022 à 17:43, Aaron Gray a écrit :
> > > 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
> >
> > --
> > François Pottier
> > francois.pottier@inria.fr
> > http://cambium.inria.fr/~fpottier/
>
>
>
> --
> Aaron Gray
>
> Independent Open Source Software Engineer, Computer Language
> Researcher, Information Theorist, and amateur computer scientist.
>

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

Re: [Caml-list] coinductive data types

[Aaron Gray]

On Tue, 30 Aug 2022 at 14:58, Nate Foster <jnfoster@cs.cornell.edu> wrote:
>
> Hi Aaron,
>
> You might be interested in looking at CoCaml. It was developed by Jean-Baptiste Jeannin as part of his PhD, in collaboration with his advisor Dexter Kozen and Alexandra Silva.
>
> https://www.cs.cornell.edu/Projects/CoCaml/

Hi Nate,

Great, thanks, I have a lot to look at in this area, a bit of a
digression, but am looking at coinductive implementations, so thanks,
hopefully I will get round to checking it out.

Aaron

> On Tue, Aug 30, 2022 at 8:38 AM Aaron Gray <aaronngray.lists@gmail.com> wrote:
>>
>> Hello François,
>>
>> Thanks for putting me straight on that.
>>
>> My original path of inquiry which I should have actually stated was
>> regarding how to go about implementing subtyping of mutually recursive
>> algebraic data types.
>>
>> I am looking on how to go about this and using coinduction and
>> bisimulation seemed like the best fit or correct way to go about this.
>>
>> Does OCaML use/handle subtyping of mutually recursive algebraic data
>> types ? And if so, is its implementation easily accessible ?
>>
>> Sorry I got you and Xavier muddled up somehow !
>>
>> Regards,
>>
>> Aaron
>>
>> On Tue, 30 Aug 2022 at 08:24, François Pottier
>> <francois.pottier@inria.fr> wrote:
>> >
>> >
>> > Hello,
>> >
>> > Le 29/08/2022 à 17:43, Aaron Gray a écrit :
>> > > 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
>> >
>> > --
>> > François Pottier
>> > francois.pottier@inria.fr
>> > http://cambium.inria.fr/~fpottier/
>>
>>
>>
>> --
>> Aaron Gray
>>
>> Independent Open Source Software Engineer, Computer Language
>> Researcher, Information Theorist, and amateur computer scientist.



-- 
Aaron Gray

Independent Open Source Software Engineer, Computer Language
Researcher, Information Theorist, and amateur computer scientist.

Re: [Caml-list] coinductive data types

[François Pottier]

Hi,

On 30/08/2022 14:37, Aaron Gray wrote:
 > My original path of inquiry which I should have actually stated was
 > regarding how to go about implementing subtyping of mutually recursive
 > algebraic data types.

Do you mean implementing an algorithm that decides whether two types are
related by subtyping, in the presence of mutually recursive algebraic
data types?

I guess the answer depends on exactly how the subtying relation is defined.
E.g., if "α foo" and "β bar" are (parameterized) algebraic data types, does
the subtyping relation "α foo ≤ β bar" necessarily imply that "foo" and 
"bar"
are the same algebraic data type?

- If the answer is positive, then the problem boils down to deciding
   "α ≤ β" or "β ≤ α" or neither or both, depending on whether this
   algebraic data type is covariant or contravariant or neither or both.
   In that case, you are working with "isorecursive" types,
   also known as "nominal" types.

- If the answer is negative, then (I imagine) you wish to unfold the
   definitions of "foo" and "bar" and decide whether the two unfoldings
   are related by subtyping.
   In that case, you are working with "equirecursive" types,
   also known as "structural" types.

Brandt and Henglein ("Coinductive axiomatization of recursive type equality
and subtyping", 1998) study the second problem, if I remember correctly.

 > Does OCaML use/handle subtyping of mutually recursive algebraic data
 > types ? And if so, is its implementation easily accessible ?

OCaml has explicit subtyping coercions: a user can write `(e : t1 :> t2)`
and the compiler will check that `t1` is a subtype of `t2`.

As far as algebraic data types are concerned, OCaml's notion of subtyping is
nominal, I believe. An algebraic data type can be decorated with variance
annotations, so, for instance, "list" can be declared covariant and "α list"
is considered a subtype of "β list" if α is a subtype of β. However, "α 
list"
can never be considered a subtype of an algebraic data type other than 
"list".

The variance annotations provided by the programmer are checked when an
algebraic data type is defined, and are later used when deciding whether a
subtyping relation holds.

Some more information here:

   https://blog.janestreet.com/a-and-a/
   https://v2.ocaml.org/manual/expr.html#ss%3Aexpr-coercions

--
François Pottier
Francois.Pottier@inria.fr
http://cambium.inria.fr/~fpottier/

Re: [Caml-list] coinductive data types

[Aaron Gray]

Hi François,

On Tue, 30 Aug 2022 at 16:47, François Pottier
<francois.pottier@inria.fr> wrote:
> On 30/08/2022 14:37, Aaron Gray wrote:
>  > My original path of inquiry which I should have actually stated was
>  > regarding how to go about implementing subtyping of mutually recursive
>  > algebraic data types.
>
> Do you mean implementing an algorithm that decides whether two types are
> related by subtyping, in the presence of mutually recursive algebraic
> data types?

Yes exactly, as well as equivalence obviously..

> I guess the answer depends on exactly how the subtying relation is defined.
> E.g., if "α foo" and "β bar" are (parameterized) algebraic data types, does
> the subtyping relation "α foo ≤ β bar" necessarily imply that "foo" and
> "bar"
> are the same algebraic data type?
>
> - If the answer is positive, then the problem boils down to deciding
>    "α ≤ β" or "β ≤ α" or neither or both, depending on whether this
>    algebraic data type is covariant or contravariant or neither or both.
>    In that case, you are working with "isorecursive" types,
>    also known as "nominal" types.
>
> - If the answer is negative, then (I imagine) you wish to unfold the
>    definitions of "foo" and "bar" and decide whether the two unfoldings
>    are related by subtyping.
>    In that case, you are working with "equirecursive" types,
>    also known as "structural" types.

I am looking at how to support both nominal and structural types in a language.
Basically at the top level with keywords 'transparent' and 'opaque',
both for type declarations,
and only narrowing 'opaque' for variable declarations and, as only
narrowing casts on value or type parameterization.

> Brandt and Henglein ("Coinductive axiomatization of recursive type equality
> and subtyping", 1998) study the second problem, if I remember correctly.

Yes I found this paper pretty early on and seems to be the founding
paper in this area, having said that, it does not seem to deal with
union and intersection types.

What I have gathered is that in order to have completeness of type
system and soundness you need the type system to be implemented as a
type lattice, there by underpinning the system on to a topological
space and thus being constructable and well founded.

>  > Does OCaML use/handle subtyping of mutually recursive algebraic data
>  > types ? And if so, is its implementation easily accessible ?
>
> OCaml has explicit subtyping coercions: a user can write `(e : t1 :> t2)`
> and the compiler will check that `t1` is a subtype of `t2`.
>
> As far as algebraic data types are concerned, OCaml's notion of subtyping is
> nominal, I believe. An algebraic data type can be decorated with variance
> annotations, so, for instance, "list" can be declared covariant and "α list"
> is considered a subtype of "β list" if α is a subtype of β. However, "α
> list"
> can never be considered a subtype of an algebraic data type other than
> "list".
>
> The variance annotations provided by the programmer are checked when an
> algebraic data type is defined, and are later used when deciding whether a
> subtyping relation holds.

Yes this is nice, covariance and contravariance annotations.

I don't know how accessible OCaML's, type system code is. I have had a
brief look, I am used to Haskell, and Haskell's type annotations in
order to get my bearings.

Are there any papers on OCaML's type system proper at all please ?

Many thanks for the comprehensive reply.

Aaron

Re: [Caml-list] coinductive data types

[François Pottier]

Hello,

Le 30/08/2022 à 18:32, Aaron Gray wrote:
 > What I have gathered is that in order to have completeness of type
 > system and soundness you need the type system to be implemented as a
 > type lattice, there by underpinning the system on to a topological
 > space and thus being constructable and well founded.

I am not sure what you mean by "soundness and completeness of the system".

A type system is considered "sound" if a well-typed program cannot crash.

A type-checking or type inference algorithm is considered "sound and 
complete"
provided it declares a program well-typed if and only if this program is
indeed well-typed. (I am simplifying the statement a bit.) This implies that
the property of being well-typed is decidable.

It is not necessary in principle for the subtyping relation to be a lattice.
The lattice property can help (e.g. it can help simplify subtyping
constraints, when performing type inference in the presence of subtyping).

 > I don't know how accessible OCaML's, type system code is. I have had a
 > brief look, I am used to Haskell, and Haskell's type annotations in
 > order to get my bearings.
 >
 > Are there any papers on OCaML's type system proper at all please ?

The code of the OCaml type-checker is publicly available but is not easy
to read.

There are several papers covering several aspects of the type system, 
but I am
not sure which one would be most relevant here. Perhaps "GADTs Meet 
Subtyping"
by Gabriel Scherer and Didier Rémy, which discusses the combination of
*generalized* algebraic data types and subtyping.

I hope this helps,

--
François Pottier
francois.pottier@inria.fr
http://cambium.inria.fr/~fpottier/

Re: [Caml-list] coinductive data types

[Andreas Rossberg]

Hi François,

I’m curious why you would categorise iso-recursive types as nominal. I have always considered them structural as well, since two structurally matching iso-recursive type expressions are still deemed equivalent. That matters in so far as it makes them modular in a way that true nominal types are not.

Iso-recursive types would only behave like nominal in the degenerate case where all type definitions occurring in the entire program (across module boundaries) are tied into a single grand iso-recursive knot, I think.

/Andreas


> On 30. 8. 2022, at 17:47, François Pottier <Francois.Pottier@inria.fr> wrote:
> 
> 
> Hi,
> 
> On 30/08/2022 14:37, Aaron Gray wrote:
> > My original path of inquiry which I should have actually stated was
> > regarding how to go about implementing subtyping of mutually recursive
> > algebraic data types.
> 
> Do you mean implementing an algorithm that decides whether two types are
> related by subtyping, in the presence of mutually recursive algebraic
> data types?
> 
> I guess the answer depends on exactly how the subtying relation is defined.
> E.g., if "α foo" and "β bar" are (parameterized) algebraic data types, does
> the subtyping relation "α foo ≤ β bar" necessarily imply that "foo" and "bar"
> are the same algebraic data type?
> 
> - If the answer is positive, then the problem boils down to deciding
>  "α ≤ β" or "β ≤ α" or neither or both, depending on whether this
>  algebraic data type is covariant or contravariant or neither or both.
>  In that case, you are working with "isorecursive" types,
>  also known as "nominal" types.
> 
> - If the answer is negative, then (I imagine) you wish to unfold the
>  definitions of "foo" and "bar" and decide whether the two unfoldings
>  are related by subtyping.
>  In that case, you are working with "equirecursive" types,
>  also known as "structural" types.
> 
> Brandt and Henglein ("Coinductive axiomatization of recursive type equality
> and subtyping", 1998) study the second problem, if I remember correctly.
> 
> > Does OCaML use/handle subtyping of mutually recursive algebraic data
> > types ? And if so, is its implementation easily accessible ?
> 
> OCaml has explicit subtyping coercions: a user can write `(e : t1 :> t2)`
> and the compiler will check that `t1` is a subtype of `t2`.
> 
> As far as algebraic data types are concerned, OCaml's notion of subtyping is
> nominal, I believe. An algebraic data type can be decorated with variance
> annotations, so, for instance, "list" can be declared covariant and "α list"
> is considered a subtype of "β list" if α is a subtype of β. However, "α list"
> can never be considered a subtype of an algebraic data type other than "list".
> 
> The variance annotations provided by the programmer are checked when an
> algebraic data type is defined, and are later used when deciding whether a
> subtyping relation holds.
> 
> Some more information here:
> 
>  https://blog.janestreet.com/a-and-a/
>  https://v2.ocaml.org/manual/expr.html#ss%3Aexpr-coercions
> 
> --
> François Pottier
> Francois.Pottier@inria.fr
> http://cambium.inria.fr/~fpottier/

Re: [Caml-list] coinductive data types

[Aaron Gray]

On Tue, 30 Aug 2022 at 17:46, Andreas Rossberg <rossberg@mpi-sws.org> wrote:
>
> Hi François,
>> I’m curious why you would categorise iso-recursive types as nominal. I have always considered them structural as well, since two structurally matching iso-recursive type expressions are still deemed equivalent. That matters in so far as it makes them modular in a way that true nominal types are not.
>
> Iso-recursive types would only behave like nominal in the degenerate case where all type definitions occurring in the entire program (across module boundaries) are tied into a single grand iso-recursive knot, I think.

Are there any founding papers or books on isorecursive and
equirecursive typing ?

Aaron

Re: [Caml-list] coinductive data types

[Nate Foster]

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

For a clear, textbook treatment of these topics at the introductory (i.e.,
advanced undergrad or beginning graduate) level, it's hard to beat Benjamin
Pierce's "Types and Programming Languages" (MIT Press, 2002). Chapters 20
and 21 cover the basics of recursive types including iso/equi-recursive
types and subtyping. And the "Notes" section at the end has lots
of references to a bunch of "founding papers" -- at least, as of 20 years
ago.

-N

On Tue, Aug 30, 2022 at 1:01 PM Aaron Gray <aaronngray.lists@gmail.com>
wrote:

> On Tue, 30 Aug 2022 at 17:46, Andreas Rossberg <rossberg@mpi-sws.org>
> wrote:
> >
> > Hi François,
> >> I’m curious why you would categorise iso-recursive types as nominal. I
> have always considered them structural as well, since two structurally
> matching iso-recursive type expressions are still deemed equivalent. That
> matters in so far as it makes them modular in a way that true nominal types
> are not.
> >
> > Iso-recursive types would only behave like nominal in the degenerate
> case where all type definitions occurring in the entire program (across
> module boundaries) are tied into a single grand iso-recursive knot, I think.
>
> Are there any founding papers or books on isorecursive and
> equirecursive typing ?
>
> Aaron
>

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

Re: [Caml-list] coinductive data types

[François Pottier]

Hi Andreas,

Le 30/08/2022 à 18:45, Andreas Rossberg a écrit :
 > I’m curious why you would categorise iso-recursive types as nominal. 
I have always considered them structural as well, since two structurally 
matching iso-recursive type expressions are still deemed equivalent.

I had in mind a system with algebraic data types, which have a name, and 
where
two algebraic data types with distinct names can never be related by 
subtyping.

In such a system, an algebraic data type is *not* equal to its 
unfolding, which
is why I used the word "iso-recursive".

It is quite possible that I used the wrong word, and should not have 
referred
to such types as "iso-recursive".

--
François Pottier
francois.pottier@inria.fr
http://cambium.inria.fr/~fpottier/

Re: [Caml-list] coinductive data types

[Peter Thiemann]

Hi François and Andreas,

this is an interesting question, which we also ran into quite recently.

Algebraic datatypes seem to conflate the isomorphism for the recursive type with the injection into a sum-of-product type for the constructors. 
They give rise to nominal types, not structural.
They are certainly not equi-recursive, because they are not equal to their unfolding.

I'd also call them iso-recursive or should they be a category by themselves?

Best
-Peter


> On 31. Aug 2022, at 10:25, François Pottier <francois.pottier@inria.fr> wrote:
> 
> 
> Hi Andreas,
> 
> Le 30/08/2022 à 18:45, Andreas Rossberg a écrit :
> > I’m curious why you would categorise iso-recursive types as nominal. I have always considered them structural as well, since two structurally matching iso-recursive type expressions are still deemed equivalent.
> 
> I had in mind a system with algebraic data types, which have a name, and where
> two algebraic data types with distinct names can never be related by subtyping.
> 
> In such a system, an algebraic data type is *not* equal to its unfolding, which
> is why I used the word "iso-recursive".
> 
> It is quite possible that I used the wrong word, and should not have referred
> to such types as "iso-recursive".
> 
> --
> François Pottier
> francois.pottier@inria.fr
> http://cambium.inria.fr/~fpottier/

Re: [Caml-list] coinductive data types

[Andreas Rossberg]

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

Hi Peter,

yes, I think they are different things. With (nominal) algebraic data types:

  type peano = Z | S of peano
  type nat = Z | S of nat
  let f (x : peano) : nat = x   -- type error

But with iso-recursive types:

  type peano = mu peano. 1 + peano
  type nat = mu nat. 1 + nat
  let f (x : peano) : nat = x   -- ok

Of course, it is merely a pragmatic choice that ML (and many other languages) treats algebraic types as nominal. It could just as well treat them as structural. In a sense, OCaml’s polymorphic variants behave more iso-recursively than its data types (at least until you activate --rectypes and opt into equi-recursive semantics).

FWIW, some old notes by Crary et al. [1] discuss this very choice, and how it interferes with modules. Moreover, based on their observations, the Harper/Stone semantics for SML actually models data type definitions as opaque abstract types (modules, really) that are merely _implemented_ by an iso-recursive type. That is both to capture their nominal (generative) semantics, but also to be able to express partial abstraction of mutually recursive types:

module type S =
sig
  type t
  type u = U of t
end

module M : S =
struct
  type t = T of u
  and u = U of t
end

This is not expressible directly with iso-recursion, as explained in [1].

(I’ve been rather interested in this topic lately, because the semantics of type recursion has been a highly contentious issue for WebAssembly, until we settled on an iso-recursive semantics. The difference between iso-recursive and nominal becomes rather crucial once you need to compile structural source types into them – then a nominal semantics in the target language essentially breaks separate compilation/linking.)

Best,
/Andreas

[1] Crary, Harper, Cheng, Petersen, Stone. Transparent and Opaque Interpretations of Datatypes, 1998 (https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.8182)


> On 31. 8. 2022, at 10:46, Peter Thiemann <thiemann@informatik.uni-freiburg.de> wrote:
> 
> Hi François and Andreas,
> 
> this is an interesting question, which we also ran into quite recently.
> 
> Algebraic datatypes seem to conflate the isomorphism for the recursive type with the injection into a sum-of-product type for the constructors. 
> They give rise to nominal types, not structural.
> They are certainly not equi-recursive, because they are not equal to their unfolding.
> 
> I'd also call them iso-recursive or should they be a category by themselves?
> 
> Best
> -Peter
> 
> 
>> On 31. Aug 2022, at 10:25, François Pottier <francois.pottier@inria.fr> wrote:
>> 
>> 
>> Hi Andreas,
>> 
>> Le 30/08/2022 à 18:45, Andreas Rossberg a écrit :
>>> I’m curious why you would categorise iso-recursive types as nominal. I have always considered them structural as well, since two structurally matching iso-recursive type expressions are still deemed equivalent.
>> 
>> I had in mind a system with algebraic data types, which have a name, and where
>> two algebraic data types with distinct names can never be related by subtyping.
>> 
>> In such a system, an algebraic data type is *not* equal to its unfolding, which
>> is why I used the word "iso-recursive".
>> 
>> It is quite possible that I used the wrong word, and should not have referred
>> to such types as "iso-recursive".
>> 
>> --
>> François Pottier
>> francois.pottier@inria.fr
>> http://cambium.inria.fr/~fpottier/
> 


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

Re: [Caml-list] coinductive data types

[François Pottier]

Le 31/08/2022 à 11:41, Andreas Rossberg a écrit :
> yes, I think they are different things. With (nominal) algebraic data types:
> 
>    type peano = Z | S of peano
>    type nat = Z | S of nat
>    let f (x : peano) : nat = x   -- type error
> 
> But with iso-recursive types:
> 
>    type peano = mu peano. 1 + peano
>    type nat = mu nat. 1 + nat
>    let f (x : peano) : nat = x   -- ok

Good point! Indeed, in the second example, peano and nat are plain
abbreviations for the same type (which happens to be a recursive
type), up to alpha-equivalence. So, not even an explicit coercion
is needed to convert x from peano to nat.

-- 
François Pottier
francois.pottier@inria.fr
http://cambium.inria.fr/~fpottier/

Re: [Caml-list] coinductive data types

[Peter Thiemann]

Hi Andreas,

> On 31. Aug 2022, at 11:41, Andreas Rossberg <rossberg@mpi-sws.org> wrote:
> 
> Hi Peter,
> 
> yes, I think they are different things. With (nominal) algebraic data types:
> 
>   type peano = Z | S of peano
>   type nat = Z | S of nat
>   let f (x : peano) : nat = x   -- type error
> 
> But with iso-recursive types:
> 
>   type peano = mu peano. 1 + peano
>   type nat = mu nat. 1 + nat
>   let f (x : peano) : nat = x   -- ok

Sure!

> 
> Of course, it is merely a pragmatic choice that ML (and many other languages) treats algebraic types as nominal. It could just as well treat them as structural. In a sense, OCaml’s polymorphic variants behave more iso-recursively than its data types (at least until you activate --rectypes and opt into equi-recursive semantics).

With "pragmatic" you mean that type checking gets more efficient or do you have some other pragmatic aspects in mind?
IIRC, polymorphic variants are just (open) sum types, which admit equi-recursion. Viz the behavior of the degenerate, one-armed polymorphic variant to "implement" iso-recursion:

# let rec m = `Fold m;;
val m : [> `Fold of 'a ] as 'a = `Fold <cycle>
# let unfold (`Fold v) = v;;
val unfold : [< `Fold of 'a ] -> 'a = <fun>


> 
> FWIW, some old notes by Crary et al. [1] discuss this very choice, and how it interferes with modules. Moreover, based on their observations, the Harper/Stone semantics for SML actually models data type definitions as opaque abstract types (modules, really) that are merely _implemented_ by an iso-recursive type. That is both to capture their nominal (generative) semantics, but also to be able to express partial abstraction of mutually recursive types:
> 
> module type S =
> sig
>   type t
>   type u = U of t
> end
> 
> module M : S =
> struct
>   type t = T of u
>   and u = U of t
> end
> 
> This is not expressible directly with iso-recursion, as explained in [1].

Thanks for the pointer to this gem!

Best
-Peter


> 
> (I’ve been rather interested in this topic lately, because the semantics of type recursion has been a highly contentious issue for WebAssembly, until we settled on an iso-recursive semantics. The difference between iso-recursive and nominal becomes rather crucial once you need to compile structural source types into them – then a nominal semantics in the target language essentially breaks separate compilation/linking.)
> 
> Best,
> /Andreas
> 
> [1] Crary, Harper, Cheng, Petersen, Stone. Transparent and Opaque Interpretations of Datatypes, 1998 (https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.8182)
> 
> 
>> On 31. 8. 2022, at 10:46, Peter Thiemann <thiemann@informatik.uni-freiburg.de> wrote:
>> 
>> Hi François and Andreas,
>> 
>> this is an interesting question, which we also ran into quite recently.
>> 
>> Algebraic datatypes seem to conflate the isomorphism for the recursive type with the injection into a sum-of-product type for the constructors. 
>> They give rise to nominal types, not structural.
>> They are certainly not equi-recursive, because they are not equal to their unfolding.
>> 
>> I'd also call them iso-recursive or should they be a category by themselves?
>> 
>> Best
>> -Peter
>> 
>> 
>>> On 31. Aug 2022, at 10:25, François Pottier <francois.pottier@inria.fr> wrote:
>>> 
>>> 
>>> Hi Andreas,
>>> 
>>> Le 30/08/2022 à 18:45, Andreas Rossberg a écrit :
>>>> I’m curious why you would categorise iso-recursive types as nominal. I have always considered them structural as well, since two structurally matching iso-recursive type expressions are still deemed equivalent.
>>> 
>>> I had in mind a system with algebraic data types, which have a name, and where
>>> two algebraic data types with distinct names can never be related by subtyping.
>>> 
>>> In such a system, an algebraic data type is *not* equal to its unfolding, which
>>> is why I used the word "iso-recursive".
>>> 
>>> It is quite possible that I used the wrong word, and should not have referred
>>> to such types as "iso-recursive".
>>> 
>>> --
>>> François Pottier
>>> francois.pottier@inria.fr
>>> http://cambium.inria.fr/~fpottier/
>> 
> 

Re: [Caml-list] coinductive data types

[Andreas Rossberg]

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



> On 31. 8. 2022, at 17:40, Peter Thiemann <thiemann@informatik.uni-freiburg.de> wrote:
> 
> Hi Andreas,
> 
>> On 31. Aug 2022, at 11:41, Andreas Rossberg <rossberg@mpi-sws.org> wrote:
>> 
>> Hi Peter,
>> 
>> yes, I think they are different things. With (nominal) algebraic data types:
>> 
>>  type peano = Z | S of peano
>>  type nat = Z | S of nat
>>  let f (x : peano) : nat = x   -- type error
>> 
>> But with iso-recursive types:
>> 
>>  type peano = mu peano. 1 + peano
>>  type nat = mu nat. 1 + nat
>>  let f (x : peano) : nat = x   -- ok
> 
> Sure!
> 
>> 
>> Of course, it is merely a pragmatic choice that ML (and many other languages) treats algebraic types as nominal. It could just as well treat them as structural. In a sense, OCaml’s polymorphic variants behave more iso-recursively than its data types (at least until you activate --rectypes and opt into equi-recursive semantics).
> 
> With "pragmatic" you mean that type checking gets more efficient or do you have some other pragmatic aspects in mind?

It probably also is easier to explain to many programmers and produces more readable error messages.

> IIRC, polymorphic variants are just (open) sum types, which admit equi-recursion. Viz the behavior of the degenerate, one-armed polymorphic variant to "implement" iso-recursion:
> 
> # let rec m = `Fold m;;
> val m : [> `Fold of 'a ] as 'a = `Fold <cycle>
> # let unfold (`Fold v) = v;;
> val unfold : [< `Fold of 'a ] -> 'a = <fun>

Yes, I think you are right that equi-recursion is still observable, but this may be the wrong example. I think it merely shows that OCaml’s let-rec is a more general fixpoint, but that also works with ordinary data types:

type t = Fold of t
let rec m = Fold m
let unfold (Fold v) = v

But the following example should reveal the underlying equi-recursive semantics:

# let f (x : [`Foo of [`Foo of 'a]] as ‘a) : [`Foo of 'b] as 'b = x;;
val f : ([ `Foo of 'a ] as 'a) -> 'a = <fun>

So yeah, strike my remark about polymorphic variants. :)


> 
> 
>> 
>> FWIW, some old notes by Crary et al. [1] discuss this very choice, and how it interferes with modules. Moreover, based on their observations, the Harper/Stone semantics for SML actually models data type definitions as opaque abstract types (modules, really) that are merely _implemented_ by an iso-recursive type. That is both to capture their nominal (generative) semantics, but also to be able to express partial abstraction of mutually recursive types:
>> 
>> module type S =
>> sig
>>  type t
>>  type u = U of t
>> end
>> 
>> module M : S =
>> struct
>>  type t = T of u
>>  and u = U of t
>> end
>> 
>> This is not expressible directly with iso-recursion, as explained in [1].
> 
> Thanks for the pointer to this gem!

Just to clarify and expand on my earlier remark, the way the Harper/Stone semantics eventually solved both problems was not by adopting “Shao’s equation” as predicted in those notes (which would require coinductive type equivalence, throwing a major advantage of iso-recursion out the window). Instead, they model the definition

  type t = A | B of t

as (the equivalent of)

  open (
    struct
      type t = mu t. 1 + t
      let A = fold (inl ())
      let B x = fold (inr x)
      let case_t x f g = match x with inl y -> f y | inr z -> g z
    end
  : sig
      type t
      val A : t
      val B : t -> t
      val case_t : t -> (unit -> 'a) -> (t -> 'a) -> ‘a
    end
  )

This explains datatypes as a combination of iso-recursion and the existing semantics for type abstraction (which could in turn be explained as existential quantification, of course :) ).

Cheers,
/Andreas


> 
> Best
> -Peter
> 
> 
>> 
>> (I’ve been rather interested in this topic lately, because the semantics of type recursion has been a highly contentious issue for WebAssembly, until we settled on an iso-recursive semantics. The difference between iso-recursive and nominal becomes rather crucial once you need to compile structural source types into them – then a nominal semantics in the target language essentially breaks separate compilation/linking.)
>> 
>> Best,
>> /Andreas
>> 
>> [1] Crary, Harper, Cheng, Petersen, Stone. Transparent and Opaque Interpretations of Datatypes, 1998 (https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.8182)
>> 
>> 
>>> On 31. 8. 2022, at 10:46, Peter Thiemann <thiemann@informatik.uni-freiburg.de> wrote:
>>> 
>>> Hi François and Andreas,
>>> 
>>> this is an interesting question, which we also ran into quite recently.
>>> 
>>> Algebraic datatypes seem to conflate the isomorphism for the recursive type with the injection into a sum-of-product type for the constructors. 
>>> They give rise to nominal types, not structural.
>>> They are certainly not equi-recursive, because they are not equal to their unfolding.
>>> 
>>> I'd also call them iso-recursive or should they be a category by themselves?
>>> 
>>> Best
>>> -Peter
>>> 
>>> 
>>>> On 31. Aug 2022, at 10:25, François Pottier <francois.pottier@inria.fr> wrote:
>>>> 
>>>> 
>>>> Hi Andreas,
>>>> 
>>>> Le 30/08/2022 à 18:45, Andreas Rossberg a écrit :
>>>>> I’m curious why you would categorise iso-recursive types as nominal. I have always considered them structural as well, since two structurally matching iso-recursive type expressions are still deemed equivalent.
>>>> 
>>>> I had in mind a system with algebraic data types, which have a name, and where
>>>> two algebraic data types with distinct names can never be related by subtyping.
>>>> 
>>>> In such a system, an algebraic data type is *not* equal to its unfolding, which
>>>> is why I used the word "iso-recursive".
>>>> 
>>>> It is quite possible that I used the wrong word, and should not have referred
>>>> to such types as "iso-recursive".
>>>> 
>>>> --
>>>> François Pottier
>>>> francois.pottier@inria.fr
>>>> http://cambium.inria.fr/~fpottier/


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

Re: [Caml-list] coinductive data types

[Basile Clement]

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

Hi Andreas,

> (I’ve been rather interested in this topic lately, because the
> semantics of type recursion has been a highly contentious issue for
> WebAssembly, until we settled on an iso-recursive semantics. The
> difference between iso-recursive and nominal becomes rather crucial
> once you need to compile structural source types into them – then a
> nominal semantics in the target language essentially breaks separate
> compilation/linking.)

This is interesting to me, do you have a pointer to these discussions
if they are public?

Best,
- Basile

> 
> Best,
> /Andreas
> 
> [1] Crary, Harper, Cheng, Petersen, Stone. Transparent and Opaque
> Interpretations of Datatypes, 1998
> (https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.8182)
> 
> 
> > On 31. 8. 2022, at 10:46, Peter Thiemann
> > <thiemann@informatik.uni-freiburg.de> wrote:
> > 
> > Hi François and Andreas,
> > 
> > this is an interesting question, which we also ran into quite
> > recently.
> > 
> > Algebraic datatypes seem to conflate the isomorphism for the
> > recursive type with the injection into a sum-of-product type for
> > the constructors. 
> > They give rise to nominal types, not structural.
> > They are certainly not equi-recursive, because they are not equal
> > to their unfolding.
> > 
> > I'd also call them iso-recursive or should they be a category by
> > themselves?
> > 
> > Best
> > -Peter
> > 
> > 
> > > On 31. Aug 2022, at 10:25, François Pottier
> > > <francois.pottier@inria.fr> wrote:
> > > 
> > > 
> > > Hi Andreas,
> > > 
> > > Le 30/08/2022 à 18:45, Andreas Rossberg a écrit :
> > > > I’m curious why you would categorise iso-recursive types as
> > > > nominal. I have always considered them structural as well,
> > > > since two structurally matching iso-recursive type expressions
> > > > are still deemed equivalent.
> > > 
> > > I had in mind a system with algebraic data types, which have a
> > > name, and where
> > > two algebraic data types with distinct names can never be related
> > > by subtyping.
> > > 
> > > In such a system, an algebraic data type is *not* equal to its
> > > unfolding, which
> > > is why I used the word "iso-recursive".
> > > 
> > > It is quite possible that I used the wrong word, and should not
> > > have referred
> > > to such types as "iso-recursive".
> > > 
> > > --
> > > François Pottier
> > > francois.pottier@inria.fr
> > > http://cambium.inria.fr/~fpottier/
> > 
> 


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

Re: [Caml-list] coinductive data types

[Andreas Rossberg]

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



> On 31. 8. 2022, at 17:55, Basile Clement <basile@clement.pm> wrote:
> 
> Hi Andreas,
> 
>> (I’ve been rather interested in this topic lately, because the semantics of type recursion has been a highly contentious issue for WebAssembly, until we settled on an iso-recursive semantics. The difference between iso-recursive and nominal becomes rather crucial once you need to compile structural source types into them – then a nominal semantics in the target language essentially breaks separate compilation/linking.)
> 
> This is interesting to me, do you have a pointer to these discussions if they are public?

Hi Basile,

it is public, but scattered around numerous issues, meeting notes, and presentations in repos of the Wasm github. Not easy to point to a single place. Happy to try digging something up if you can narrow down what specifically you are interested in. (I suggest you mail me off-list, though, since it’s probably off-topic here.)

Cheers,
/Andreas


> 
> Best,
> - Basile
> 
>> 
>> Best,
>> /Andreas
>> 
>> [1] Crary, Harper, Cheng, Petersen, Stone. Transparent and Opaque Interpretations of Datatypes, 1998 (https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.8182 <https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.8182>)
>> 
>> 
>>> On 31. 8. 2022, at 10:46, Peter Thiemann <thiemann@informatik.uni-freiburg.de <mailto:thiemann@informatik.uni-freiburg.de>> wrote:
>>> 
>>> Hi François and Andreas,
>>> 
>>> this is an interesting question, which we also ran into quite recently.
>>> 
>>> Algebraic datatypes seem to conflate the isomorphism for the recursive type with the injection into a sum-of-product type for the constructors. 
>>> They give rise to nominal types, not structural.
>>> They are certainly not equi-recursive, because they are not equal to their unfolding.
>>> 
>>> I'd also call them iso-recursive or should they be a category by themselves?
>>> 
>>> Best
>>> -Peter
>>> 
>>> 
>>>> On 31. Aug 2022, at 10:25, François Pottier <francois.pottier@inria.fr <mailto:francois.pottier@inria.fr>> wrote:
>>>> 
>>>> 
>>>> Hi Andreas,
>>>> 
>>>> Le 30/08/2022 à 18:45, Andreas Rossberg a écrit :
>>>>> I’m curious why you would categorise iso-recursive types as nominal. I have always considered them structural as well, since two structurally matching iso-recursive type expressions are still deemed equivalent.
>>>> 
>>>> I had in mind a system with algebraic data types, which have a name, and where
>>>> two algebraic data types with distinct names can never be related by subtyping.
>>>> 
>>>> In such a system, an algebraic data type is *not* equal to its unfolding, which
>>>> is why I used the word "iso-recursive".
>>>> 
>>>> It is quite possible that I used the wrong word, and should not have referred
>>>> to such types as "iso-recursive".
>>>> 
>>>> --
>>>> François Pottier
>>>> francois.pottier@inria.fr <mailto:francois.pottier@inria.fr>
>>>> http://cambium.inria.fr/~fpottier/
>>> 
>> 
> 


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