Re: [Caml-list] coinductive data types

[Andreas Rossberg <rossberg@mpi-sws.org>]

[-- 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 --]