Re: no names allowed, we serve types only

From: Keith H Duggar <>
Date: Sun, 21 Feb 2010 08:30:28 -0800 (PST)
Message-ID: <>

On Feb 21, 6:05 am, Jan Hidders <> wrote:
> Btw. was the typing rule for equality already discussed? That's not as
> straightforward as some might think. One proposal could be that t1 =
> t2 is allowed if t1 and t2 have at least one common supertype. Or
> should that be subtype? Or both? :-) The right answer depends on
> several things such as the chosen semantics of your types; two types
> would be semantically incomparable if the intersection of their
> semantics is empty. I can easily imagine that the schema designer
> should be able to indicate explicitly that two types are incomparable,
> even though they would be semantically comparable.

Unless I've lost track, it was only briefly discussed

in the context of operator specifications in general. So a type system could allow fine grained control over the signatures that are implicity/explicity allowed with/without coersion. In the example below I'm going to continue using "copy" to denote the declaration of a "strong" type alias ie it creates a distinct type not just another name for same type. So let's suppose we define X and Y coordinates type as copies of an Integer type

   copy Integer X
   copy Integer Y

and that by default the type system does not supply implicit coersion nor the multi-sorted equality operators. Then we would explicity add those multi-sorted signatures

  • : X, Y -> bool
  • : Y, X -> bool

to the type system. This would allow X and Y equality comparison. Now suppose elsewhere we have defined a part count

   copy Integer PartCount

but do not add the multi-sorted (with X and Y) equality operators. Then PartCount will not by default be equality comparable to X and Y. This allows one to control the semantics.

One can also easily create various groups of semantically related types to allow convenient shortcuts. For example, if we have more than just two coordinates say we add Z, W, T it would be annoying to explicity define the equality signatures for all permutations of those types even though we want them to be comparable. So we first create a Coordinate type then copy it

   copy Integer Coordinate
   copy Coordinate X
   copy Coordinate Y
   copy Coordinate Z
   copy Coordinate W
   copy Coordinate T

and now explicity add implicit coersion signatures

   () : X -> Coordinate
   () : Y -> Coordinate
   () : Z -> Coordinate
   () : W -> Coordinate
   () : T -> Coordinate

which now allows implicit mutual equality comparison (and any other operators) between X, Y, Z, W, T and Coordinate since they are now implicitly coerced to Coordinate. Here we only had to explicitly add only a linear number of implicit coersion operators instead of a combinatorial number of equality signatures.

KHD Received on Sun Feb 21 2010 - 17:30:28 CET

Original text of this message