[TYPES] a naive question on datatype declarations

[Jon Sterling]

Thorsten — The use of abstract types to formally distinguish two copies of the "same" data type is precisely the thing that avoids observing anything about a datatype beyond its isomorphism class, and this does certainly not imply introducing tags. Your proposed solution, to introduce tags in order to distinguish two different intended uses of a datatype, is far too strong and is unnecessary. Indeed, with tags, you would be able to show the negation of "AgeInt = LengthInt" or something, but all that is needed to answer Gershom's question is that we "AgeInt = LengthInt" be non-derivable. In the past, certain systems have implemented abstraction by means of tags, but that is not necessary; the simplest implementation of abstraction is a form of let-binding, which obviously introduces no notion of tag — and is compatible neither "AgeInt = LengthInt" nor "Not(AgeInt = LengthInt)" being derivable, as is desirable in the present discussion.

I would say that the concept of tags is a separate one that has deep and interesting theory and applications, as Jonathan Aldrich has pointed out. But type abstraction does not imply tagging — not even "static" tagging. Tagging is important when you want to be able to actually negate the identification of two differently-tagged types. Negation is not the same thing as failure.

Best,
Jon


> On Jan 28, 2024, at 6:52 PM, Thorsten Altenkirch <Thorsten.Altenkirch at nottingham.ac.uk> wrote:
> 
> Hi,
>  
> This doesn’t make sense to me: datatypes are not abstract types hence why should they “treated” as such?
>  
> From a semantic point of view all that we should be able to observe of a datatype is its isomorphism class. Now in applications we want to distinguish different uses of a datatype, e.g. an integer may represent an age or the number of eggs. This is a different beast it is a type together with a tag (or a dimension). It doesn’t seem right to confuse the two things.
>  
> Cheers,
> Thorsten
>  
> From: Types-list <types-list-bounces at LISTS.SEAS.UPENN.EDU <mailto:types-list-bounces at LISTS.SEAS.UPENN.EDU>> on behalf of Jon Sterling <jon at jonmsterling.com <mailto:jon at jonmsterling.com>>
> Date: Saturday, 27 January 2024 at 15:25
> To: types-list at LISTS.SEAS.UPENN.EDU <mailto:types-list at LISTS.SEAS.UPENN.EDU> <types-list at LISTS.SEAS.UPENN.EDU <mailto:types-list at LISTS.SEAS.UPENN.EDU>>
> Subject: Re: [TYPES] a naive question on datatype declarations
> 
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> Hi Gershom,
> 
> This is a good question, and often overlooked. Bob Harper taught me to think of these things as abstract types, and I agree — so the thing that makes two different datatype declarations different is the existing abstraction mechanism of your language. When you think of it this way, you think of the pattern-matching forms as being elaborated to some kinds of destructors or combinators — which are themselves part of the abstract interface of the type.
> 
> I cannot confirm because I don't remember the code, but it may be that the TILT compiler actually worked this way. Probably Bob will have a fresher recollection of this.
> 
> Best,
> Jon
> 
> 
> On Fri, Jan 26, 2024, at 10:18 PM, Gershom B 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
> This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law.