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