[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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 <gersh...@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