Re: An alternative to possreps

From: David BL <davidbl_at_iinet.net.au>
Date: Sun, 29 May 2011 23:35:30 -0700 (PDT)
Message-ID: <2be6992e-4372-4adb-a9d5-1291efcfc5d6_at_d26g2000prn.googlegroups.com>


On May 29, 8:34 pm, Eric <e..._at_deptj.eu> wrote:
> On 2011-05-27, David BL <davi..._at_iinet.net.au> wrote:
>
> > The purpose of this post is to outline an alternative to POSSREPS for
> > distinguishing between a type and the physical representation of
> > values of that type on a system.
>
> I am beginning to think you are trying to solve a problem that doesn't
> really exist.

It's an alternative to possreps. I think it's neither more nor less powerful.

However it's clearly much simpler. I think possreps raise more questions than my proposal. Here are some off the top of my head after reading Date's Introduction book:

  1. Do union types (and particularly dummy types) contradict Date's statement that every type has at least one possible representation? How does it fit in with the claim that the set of values of a given type must be well defined?
  2. What are dummy types for? Can dummy types have subtype relationships declared amongst them? If so what happens with CONSTRAINT declarations? Aren't these always required when expressing subtype as specialisation by constraint?
  3. Must POSSREPSs have a canonical representation? What happens if I don't want the selector RATIONAL(numerator,denominator) to have a constraint on the two given integers apart from a nonzero denominator? What happens if I can much more easily define equivalence than a constraint that forces a canonical representation? Is equality implicitly defined at the logical level? If so what exactly are the assumptions that allow for the definition of logical equality to be implied? Alternatively is it up to the implementation to define the equality operator (just like the implementation of any other operator)?
  4. Can preconditions be declared on operators? If so would it be true to say it seems to overlap in purpose with CONSTRAINT declarations?
  5. Can additional POSSREPS be added to a type without modifying the original declaration of that type? Can a new supertype be added to the type system without needing to modify the definitions of all its subtypes?
  6. Are covariant return types supported?
  7. For the types, operators and subtype relationships that comprise a type system, the way in which it is expressed using POSSREPS, dummy types, free standing operators and so forth doesn't appear to be uniquely defined. Is there a recommended methodology? What makes one POSSREP more desirable than another? What is the purpose of defining multiple POSSREPS? Is it just a way to provide more operators? What's wrong with adding free standing operators instead? In practise would POSSREPs be expected to provide hints for implementations or is that not really an intention?
  8. Is it possible to add super-types to the built-in types?
  9. Do TYPE and POSSREP definitions express more information than simply declaring the existence of types, subtype relationships and operators? If so what is contained in this additional information and what is it for? How does one avoid repetition when specifying both logical and physical representations for a given type, or is that not an issue?

My proposal has the effect of treating specialisation by constraint as simply part of the problem of defining equivalence classes on logical representations. If the system leaves it up to the hidden implementation to define the equality operator, the DDL is simpler. For example, there is no need for the DDL to somehow express the fact that for all radius R and centre C

    circle(R,C) = ellipse(R,R,C)

Note that Date requires a definition of CIRCLE to have a constraint declared like this:

    CONSTRAINT THE_A(ELLIPSE) = THE_B(ELLIPSE) My understanding is that many of the implementations inspired by TTM have yet to implement subtyping by constraint. I think at the moment it's reasonable to require implementations of user defined types to define the equality operator rather than have it generated automatically. This is probably a good approach in computational geometry where data types can be rather complex (e.g. triangulated surfaces) and manually written comparison operators are appropriate.

> > we can represent any natural number starting from 0 and using the
> > successor operator s as many times as required:
>
> > 1 is logically represented by s(0)
> > 2 is logically represented by s(s(0))
> > 3 is logically represented by s(s(s(0)))
> > etc
>
> Well, so we can, but why do it in this context? You can't go back to
> first principles in everything every time, not if you want to end up
> with something usable.

The purpose here was only to illustrate the idea that the declared types, subtype declarations and operator signatures define a grammar for logical expressions, where operator signatures are analogous to production rules of formal language grammars. It was also a good example to clarify the distinction between logical and physical representations of values. Obviously in practise a system would provide built-in types and allow for syntactic sugar for representing literals like 100, 1.5e04, "hello world", {1,2,3}, [1,2,3] etc. Received on Mon May 30 2011 - 08:35:30 CEST

Original text of this message