[TYPES] a naive question on datatype declarations

[Richard Eisenberg]

Hi Gershom,

I'm not sure how useful it will be for your goals here, but my co-authored paper "Kind Inference for Datatypes <https://urldefense.com/v3/__https://dl.acm.org/doi/10.1145/3371121__;!!IBzWLUs!VLMhoiZ94plx6x0iiMBjOeUBZ-eWBZ6CG04adL5f5Awaf_cEmgvlKAhLoSuKUDSM4e1L20VY0_pWHzWibtZuSJeX-ugfLw$ >" (POPL'20) has some structure that resembles what you're looking for. It has a treatment of the surface syntax. But it focuses on inference (as the title suggests) and does not relate the surface definitions to structural isorecursive types in a core calculus. I don't believe the paper addresses type soundness. But I do remember while working on this that I was surprised there wasn't more treatment of the issues you're describing in the literature. I think it's an overlooked corner.

Richard

> On Jan 29, 2024, at 3:34 PM, Gershom B <gershomb at gmail.com> wrote:
> 
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> Thanks all for the great responses.
> 
> I'll give a bit more context what we're doing and what I'm looking
> for, though judging from the responses thus far I don't think it
> currently exists.
> 
> We have a system with the usual type-formers and also iso-recursive
> types (and of course some novel features), and a model that shows the
> soundness of this system, etc. Now, what would be great is if there is
> a result that lets us say "for such a system, there a related system
> that also has explicit recursive datatype declarations of the form of
> ML or Haskell98 [etc], and there is a simple translation such that
> results done with iso-recursive types lift easily into the system with
> explicit datatypes declarations."
> 
> Extensionals / module-based approaches seem a powerful approach to the
> modeling, but likely overkill what we'd like to be able to say, which
> would likely be able to be done largely on a syntactic level.
> 
> That said, it appears that most people are content to sort of
> "hand-wave" that a proof in an iso-recursive setting is enough to "say
> something" (even if not in a formal proof sense) about systems with
> explicit datatype declarations, and given the current state of
> literature, I hope an audience would find that reasonable? That is to
> say -- our motivations in studying these things relate to existing
> languages and implementations -- and in those, we use explicit
> datatype declarations. So one hopes that limiting ourselves to instead
> iso-recursive types does not undercut this motivation too drastically.
> 
> Best,
> Gershom
> 
> 
> 
> On Sun, Jan 28, 2024 at 1:12 PM Sandro Stucki <sandro.stucki at gmail.com> wrote:
>> 
>> Hi Gershom,
>> 
>> That's not a naive question at all, in my opinion. :-)
>> 
>> In addition to the many useful answers provided by others, I wanted to
>> mention Christopher Stone's Chapter on "Type Definitions" (Chapter 9)
>> in Advanced Topics in Types and Programming Languages (ATAPL). It
>> describes a number of different approaches for adding type definitions
>> in an F-omega-style type system, with calculi to illustrate them and a
>> discussion of the meta-theoretic issues, TAPL-style. I found it very
>> useful when I started to learn about this topic for my own research.
>> 
>> Cheers,
>> Sandro
>> 
>> 
>> On Sat, Jan 27, 2024 at 3:34 AM Gershom B <gershomb at gmail.com> wrote:
>>> 
>>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>>> 
>>> In typical treatments of languages with recursive types, we present a
>>> syntax with either isorecursive or equirecursive types. But we do not
>>> have a syntax for introduction of type declarations.
>>> 
>>> This is to say that we assemble types out of constructors for e.g.,
>>> polymorphism, recursion, sum, product, unit, exponential (give or
>>> take).
>>> 
>>> But we do not have the equivalent of a "data" declaration in Haskell
>>> that lets us explicitly say
>>> 
>>> data Bool = True | False
>>> 
>>> or
>>> 
>>> data List a = Nil | Cons a
>>> 
>>> It is, I suppose, expected that readers of these papers can think
>>> through how to translate any given data datatypes in languages with
>>> explicit declaration into the underlying fixed type calculus.
>>> 
>>> However, I am curious if there is any reference for *explicit*
>>> treatment of the syntax for datatype declarations and semantic
>>> modeling of such?
>>> 
>>> One reason for such would be that in the calculi I described above,
>>> there's of course no way to distinguish between the above `data Bool`
>>> and e.g. `1 + 1`, while it might be desirable to maintain that strict
>>> distinction between actual equality and merely observable isomorphism.
>>> 
>>> Thanks,
>>> Gershom