[TYPES] a naive question on datatype declarations

[Gershom B]

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