[TYPES] a naive question on datatype declarations

[Jonathan Aldrich]

In addition to the excellent answers already provided, I wanted to mention
that one way to model datatype cases is with globally unique tags that
exist at both compile time and run time.  This solution is useful if you
want the tags to have a unique, testable run-time representation, as in
dynamically typed or gradually typed languages, or in any object-oriented
language with a single-rooted class hierarchy.

For example, if you have a variable of type any (i.e. Top), you can do a
dynamic tag check to see if the value it holds is a True, and in the
appropriate case of the pattern match you'd gain static knowledge that the
value has type True (and thus also Boolean by subsumption).  This would
make Bool different from 1+1 both statically and dynamically.

Lee, Shaw, Potanin, and I developed a theory of tagged objects to account
for this:

A Theory of Tagged Objects. Joseph Lee, Jonathan Aldrich, Troy Shaw, and
Alex Potanin. Proc. European Conference on Object-Oriented Programming
(ECOOP), 2015.  https://urldefense.com/v3/__https://www.cs.cmu.edu/*aldrich/papers/ecoop15-tags.pdf__;fg!!IBzWLUs!Rypoowc_ByaoAzG_LHVOBno644cTgPmq_0t3L9DYaKNwWBTO_kQeNdUeFZBDD79qpl-VL6o5FUM9dFjdIKh_Bw0O3HO79LzspE1S_ua9sQ$ 

The theory unifies approaches to tags in object-oriented and functional
programming.

Best,

Jonathan Aldrich

On Fri, Jan 26, 2024 at 9:38 PM 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
>