Re: User-defined type attributes

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Thu, 13 Mar 2008 20:55:27 -0700 (PDT), Eric Hughes wrote:

> On Mar 13, 1:58 pm, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
> wrote:
>> In which sense function is static? If understand what you wrote, it simply
>> means that the name "Callable" is static.
> 
> That's not what I meant.  Here's some sample notation, whose syntax is
> merely illustrative.
> 
>     -- Declaration of an attribute
>     generic
>         task type T ;
>     function T'Callable return boolean ;
> 
>     -- Declaration of a (static) implementation function
>     generic
>         task type T ;
>     function Callable_Impl return access function( X : T ) return
> boolean is static ;

Hmm, what is static here? An instance of the body or the result of
execution of an instance? Let I declare T in a nested block, then
instantiate Callable_Impl there, would it go?

>     -- Binding of an implementation to an attribute
>     generic
>         task type T ;
>         Obj : T ;
>     for Obj'Callable use Callable_Impl.all( X => Obj ) ;
> 
> Regardless of whatever syntax is appropriate, one of the things that
> makes me uncomfortable about attributes is that their definitions
> don't have the same rigor of notation in their definitions as, say,
> the standard libraries do.

Right, because to make it rigorously you have to make "task type" a proper
class. That means, tasks must be tagged, there must be Root_Task type and a
class of. Then you could simply and rigorously write:

   function "'Callable" (T : Root_Task) return Boolean;

> In the spirit of separation compilation,
> I'd like to see attribute definitions in specification packages, even
> if their bodies exist solely within a compiler's implementation.

Sure. Nevertheless this or that way you have to be able to specify that a
body is static (contract on the implementation). That the body is pure (a
permission to derive static result from static arguments). Or do you want
compile-time bodies written in some other (meta) language, like they are in
C and PL/1 preprocessors?

> I wrote:
>> Functions on a type are part of the tradition algebraic
>> specification of a type.  Attributes on a type are part of the
>> language environment inside of which a type specification is
>> expressed.  These are very different.
> 
> "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de> wrote:
>> I don't see why this distinction is important.
> 
> I'm afraid I don't know how to argue this point briefly.  It's the
> difference between language (in the proof theory sense) and
> metalanguage.  I guess I've done too much formal logic too see this
> distinction and its import as anything other than obvious.

I see where you are going. It is to consider (some) attributes
automatically instantiated generic functions. Am I right?

That would be indeed a metalanguage. But I am quite uncomfortable with all
three: metalanguage, generics as one, automatic instantiation. As you said,
a metalanguage shall be clearly separated from the object one. This is the
reason why generics are bad, they slip through the barrier and exist at run
time. Similarly attributes inevitably will.

IMO it would much "simpler" (and more useful):

1. to make classes available for all types
2. to introduce pure and static bodies
3. to allow "'X" sugar for user-defined subprograms
4. to specify existing attributes in terms of 1..3.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de