[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hi Thorsten, I don't know what to tell you, since I'm describing nothing more than the rule of contraction in logic / type theory — which is the essence of abstraction (temporarily viewing two identical things as different). If you want to dispute about whether this is semantically meaningless or a "hack", go ahead — but I think I'm going to bow out of the discussion. Gershom by now has gotten a variety of very interesting and helpful answers. Best, Jon > On Jan 29, 2024, at 9:32 AM, Thorsten Altenkirch > <[email protected]> wrote: > > What does it mean to introduce two copies of the same datatype? > > And if we can’t show AgentInt != LengthInt can we show not( AgentInt != > LengthInt)? > > It seems to me your suggestion is just a hack abusing an existing language > feature but it is semantically meaningless. > > Thorsten > > From: Jon Sterling <[email protected]> > Date: Monday, 29 January 2024 at 08:24 > To: Thorsten Altenkirch (staff) <[email protected]> > Cc: [email protected] <[email protected]> > Subject: Re: [TYPES] a naive question on datatype declarations > > 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 > <[email protected]> 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 <[email protected] > <mailto:[email protected]>> on behalf of Jon Sterling > <[email protected] <mailto:[email protected]>> > Date: Saturday, 27 January 2024 at 15:25 > To: [email protected] <mailto:[email protected]> > <[email protected] <mailto:[email protected]>> > 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. > > 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.
