[TYPES] a naive question on datatype declarations

[Kalani Thielen]

Hi Gershom,

Just mentioning in case I missed a more subtle point, I assume your “List” definition was meant to be “data List a = Nil | Cons a (List a)” (which is what makes it recursive where Bool is not).

If I understand your question correctly, you’d like to distinguish the structural type ‘1+1’ from the nominal type ‘Bool=1+1’ in a way that’s consistent with structural type checking?

There’s more than one way to do it, but the way I’ve usually done it is to have a type constructor for “primitives” take an optional representation type, so to form a type you could say e.g. ‘Primitive “Bool” (1+1)’, and a value of such type by ‘1+1’ but distinguished from that type (requiring use of in/out functions to construct or deconstruct, similar to what you’d already do with roll/unroll for iso-recursive types).

I’m not certain of your motivation for the question so I don’t want to assume, but the reason I went down this path was to keep as much of the “meaning” of types explicit in their structure so that it’s always locally available, and not spread out in other bits of compiler state.

Another aspect of this problem (IMHO) is in the variant labels for your types.  In Haskell, when you say “data Bool = True | False” then (in the same scope) you can never use the constructor names “True” or “False” again (obviously this is dual to record field labels, where people are usually much less tolerant of this restriction).  I prefer to lift those names into the structure of a variant type as well, using a syntax like “|True:1, False:1|”, and for iso-recursive types I use a syntax like “^x.1+(int*x)” (these syntax choices are dirty deeds) and the usual “\x.T” for type-level functions, so together your “List” type would look something like:

Primitive “List” (\a.^x.|Nil:1, Cons:(a*x)|)

I hope that this is helpful in some way.  Please correct me if I’ve misunderstood your question.

BTW we met at the CUNY HoTT reading group some years ago, good to read you again.  I was working on a PL for Morgan Stanley at the time (too practical for some folks there), which is where I used the approach above.



> On Jan 26, 2024, at 5:18 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