[TYPES] a naive question on datatype declarations

[Sandro Stucki]

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