Is ParaSail type system sound and fast?

[Zing Chen]

Park Gyunghee et al. in a recent work [1] presented a type-sound language supporting generics, covariance/contravariance, multiple symmetrically dispatching parameters (a la Ada 95) and multiple interface inheritance (a la Ada 05). According to authors, their work concludes a long-standing research on object-oriented type systems.

The authors are serious about efficiency, but they admit that they're willing to "accept exponential blow-ups" (presumably in dynamic type resolution, i.e. method lookup at run-time), although "techniques like caching or dynamic compilation can help". In my humble understanding, their work demonstrates that in certain areas like hard real-time programming, object orientation in full generality is a dead end.

They mentioned ParaSail as one of related works.

I wonder if ParaSail is type-sound and whether it supports constant-time method lookup.

Thank you for your attention.

[1] G Park et al.:Polymorphic Symmetric Multiple Dispatch with Variance. 2019.

https://popl19.sigplan.org/event/popl-2019-research-papers-polymorphic-symmetric-multiple-dispatch-with-variance

[Tucker Taft]

Yes, ParaSail is type-sound and supports constant-time method lookup, including when calling through interfaces.  I'd be happy to elaborate if your are interested.  The most recent publication on ParaSail is at:

  https://programming-journal.org/2019/3/7/

PDF at: https://arxiv.org/pdf/1902.00525v1

This paper doesn't discuss the issue of constant-time method lookup specifically, but I'd be happy to elaborate if you had any questions.  ParaSail shares a feature with Ada 95 in its handling of operations with multiple operands that control dispatching, using covariance consistently for all parameters and for the result type.  This approach is simpler to understand in my experience, and matches the normal way that operators like "+" work for abstract data types.  ParaSail has a somewhat more efficient approach than Ada 2005 to handling multiple inheritance from interfaces, allowing method lookup to be constant time.

The ParaSail reference manual is at: https://adacore.github.io/ParaSail/images/parasail_ref_manual.pdf

If you'd like to download ParaSail, visit http://parasail-lang.org

Take care,

-Tucker Taft

--
You received this message because you are subscribed to the Google Groups "ParaSail Programming Language" group.
To unsubscribe from this group and stop receiving emails from it, send an email to parasail-programming...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Zing Chen]

Thank you for your answer. I guess I should not ask more questions before re-reading the materials carefully. But, as an average programmer, I wish to see more application-level documentation -- how things should be written, how are they implemented, code/data layout, metrics, and so forth. And what's more, I would love to see ParaSail illustrated in comparison with a well-known language targeting the same domain. C++ would be best.

To the topic, I'm not sure we are talking about the same kind of covariance/contravariance. The term "variance" in [1] refer to that of generic type construction. For example, one may want to define a generic type Function<Domain,Range> such that Function<Y,X> is a "subtype" of Function<X,Y> (i.e. an object of Function<Y,X> can be used in every context expecting an object of Function<X,Y>) whenever X is a "subtype" of Y. Such a generic Function<Domain,Range> type has to be declared contravariant on the Domain argument type and covariant in the Range argument type. ParaSail, according to [1], does not allow this kind of definition, unless of course X = Y, and is thus considered "invariant".

Thank you.

On Monday, April 22, 2019 at 1:09:04 AM UTC+7, Tucker Taft wrote:

Yes, ParaSail is type-sound and supports constant-time method lookup, including when calling through interfaces.  I'd be happy to elaborate if your are interested.  The most recent publication on ParaSail is at:

  https://programming-journal.org/2019/3/7/

PDF at: https://arxiv.org/pdf/1902.00525v1

This paper doesn't discuss the issue of constant-time method lookup specifically, but I'd be happy to elaborate if you had any questions.  ParaSail shares a feature with Ada 95 in its handling of operations with multiple operands that control dispatching, using covariance consistently for all parameters and for the result type.  This approach is simpler to understand in my experience, and matches the normal way that operators like "+" work for abstract data types.  ParaSail has a somewhat more efficient approach than Ada 2005 to handling multiple inheritance from interfaces, allowing method lookup to be constant time.

The ParaSail reference manual is at: https://adacore.github.io/ParaSail/images/parasail_ref_manual.pdf

If you'd like to download ParaSail, visit http://parasail-lang.org

Take care,

-Tucker Taft

[Tucker Taft]

An important thing to understand about both ParaSail and Ada 95, 2005, and 2012, is that they distinguish between "specific" types like "T" and the set of types that are derived from T, directly or indirectly.  In ParaSail, that set is denoted by "T+".  In Ada, it is denoted by "T'Class".  In ParaSail, T+ is called a "polymorphic" type, and a parameter of type T+ can accept T or any type derived from T.  In Ada, it is called a "class-wide" type.  Run-time dispatching only occurs when you have an actual parameter of a polymorphic/class-wide type, and you pass it to an operation of the "root" type of the set of types (T in this case).  Because of the rules of inheritance, all operations of the root type have corresponding operations in the derived types, either by inheriting an operation, or by overriding an operation with a new definition.  All of this is pretty similar to C++, Java, etc., except that ParaSail/Ada provide static binding when operands are all of a "specific" type, and only does dynamic binding when the operands are polymorphic/class-wide.  In C++, a similar distinction exists, but it is based more on whether the object is identified by a pointer vs. identified by a stack-resident object.

In any case, the terms "covariance" and "contravariance" I am familiar with have to do with how the types of the formal parameters of an operation are adjusted upon inheritance and for the purposes of overriding.  The general rule is you can override using "contravariance" in the parameter types, and "covariance" in the result type.  In ParaSail and Ada, covariance is used in all cases.  This is sound because on dynamically dispatched calls, all parameters that "control" dispatching are required to be of the same type, which is checked at run-time if necessary.  Unlike in most languages, there is no single controlling parameter.  All parameters that are of the "controlling" type are treated symmetrically.

WikiPedia has a longer discussion of covariance and contravariance:

   https://en.wikipedia.org/wiki/Covariance_and_contravariance_(computer_science)#Inheritance_in_object-oriented_languages

It is the discussion about inheritance in object-oriented languages that is most relevant.

I realize this might not have answered your question, so feel free to send a follow-up.  I also encourage you to download the release, look at the extensive examples, read the reference manual, etc.

Take care,

-Tuck

[Zing Chen]

On Monday, April 22, 2019 at 11:44:05 PM UTC+7, Tucker Taft wrote:

An important thing to understand about both ParaSail and Ada 95, 2005, and 2012, is that they distinguish between "specific" types like "T" and the set of types that are derived from T, directly or indirectly.  In ParaSail, that set is denoted by "T+".  In Ada, it is denoted by "T'Class".  In ParaSail, T+ is called a "polymorphic" type, and a parameter of type T+ can accept T or any type derived from T.  In Ada, it is called a "class-wide" type.  Run-time dispatching only occurs when you have an actual parameter of a polymorphic/class-wide type, and you pass it to an operation of the "root" type of the set of types (T in this case).  Because of the rules of inheritance, all operations of the root type have corresponding operations in the derived types, either by inheriting an operation, or by overriding an operation with a new definition.  All of this is pretty similar to C++, Java, etc., except that ParaSail/Ada provide static binding when operands are all of a "specific" type, and only does dynamic binding when the operands are polymorphic/class-wide.  In C++, a similar distinction exists, but it is based more on whether the object is identified by a pointer vs. identified by a stack-resident object.

In any case, the terms "covariance" and "contravariance" I am familiar with have to do with how the types of the formal parameters of an operation are adjusted upon inheritance and for the purposes of overriding.  The general rule is you can override using "contravariance" in the parameter types, and "covariance" in the result type.  In ParaSail and Ada, covariance is used in all cases.  This is sound because on dynamically dispatched calls, all parameters that "control" dispatching are required to be of the same type, which is checked at run-time if necessary.  Unlike in most languages, there is no single controlling parameter.  All parameters that are of the "controlling" type are treated symmetrically.

Thank you for the lesson about dispatching. I'm familiar with the mechanism and notations T+, T'Class, but I'm always happy and honored to learn it from the creator of the languages. I really appreciate this.

WikiPedia has a longer discussion of covariance and contravariance:

   https://en.wikipedia.org/wiki/Covariance_and_contravariance_(computer_science)#Inheritance_in_object-oriented_languages

It is the discussion about inheritance in object-oriented languages that is most relevant.

I realize this might not have answered your question, so feel free to send a follow-up.  I also encourage you to download the release, look at the extensive examples, read the reference manual, etc.

Very clear. I have no question about this kind of covariance. But I'll take opportunity to re-formulate my previous question, in a simpler way. Let Queue<T> be a generic class describing a queue of T (the type of elements of the queue). Is there any relation between Queue<TCP> and Queue<IP>, two instances of Queue<T>, if type TCP extends (i.e. is derived from) type IP?

Thank you.

[Tucker Taft]

On Mon, Apr 22, 2019 at 2:05 PM Zing Chen <tranng...@gmail.com> wrote:

...

Very clear. I have no question about this kind of covariance. But I'll take opportunity to re-formulate my previous question, in a simpler way. Let Queue<T> be a generic class describing a queue of T (the type of elements of the queue). Is there any relation between Queue<TCP> and Queue<IP>, two instances of Queue<T>, if type TCP extends (i.e. is derived from) type IP?

When you declare Queue, you have to specify something about "T."  You might want it to be merely Assignable, or perhaps Comparable or Hashable or Imageable.  E.g.:

    interface Queue<T is Comparable<>> is

       ...

    end interface Queue

At some later point, you could define another interface that required a Queue, and at that point, you could further constrain "T", so you could write:

    interface Queuing_System<Network_Q is Queue<T => IP<>>> is ...

by specifying some limitations on T in the formal type for Network_Q we limit what sort of Queue can be passed when instantiating Queuing_System.  Hence the following is an illegal instantiation of Queuing_System:

       type Simple_Queuing_System is

          Queuing_System<Network_Q => Queue<Integer>>  // Illegal

whereas this is a legal instantiation:

     type Better_Queuing_System is

         Queuing_System<Network_Q => Queue<TCP>>  // Legal

I hope that at least partially addresses your question.

Thank you.

Take care,

-Tuck

[Zing Chen]

I meant whether it is possible to use a Queue<TCP> object where a Queue<IP> object is expected, for example

Process_Queue(qIP);
Process_Queue(qTCP);

where qIP is a queue of IP elements (probably declared as Queue<IP> or Queue<IP+> or Queue<IP>+) and, similarly, qTCP is a queue of TCP elements.

In order to be so, Queue<TCP> has to be a "subtype" or "supertype" of Queue<IP> by language definition. As ParaSail follows Ada model, I don't think that's possible (unless of course TCP is equivalent to IP).

Is my guess correct?

Thank you.

On Tuesday, April 23, 2019 at 2:55:02 AM UTC+7, Tucker Taft wrote:

[Tucker Taft]

On Tue, Apr 23, 2019 at 5:06 AM Zing Chen <tranng...@gmail.com> wrote:

I meant whether it is possible to use a Queue<TCP> object where a Queue<IP> object is expected, for example

Process_Queue(qIP);
Process_Queue(qTCP);

where qIP is a queue of IP elements (probably declared as Queue<IP> or Queue<IP+> or Queue<IP>+) and, similarly, qTCP is a queue of TCP elements.

In order to be so, Queue<TCP> has to be a "subtype" or "supertype" of Queue<IP> by language definition. As ParaSail follows Ada model, I don't think that's possible (unless of course TCP is equivalent to IP).

Is my guess correct?

There are two places in ParaSail where one type can "substitute" for another.  One is as an actual parameter in a function call.  The second is as a parameter to a module instantiation.  In the former, the only "substitutions" are as part of a call where the formal parameter is explicitly a polymorphic type like Queue<IP>+.  In that case, you can substitute Fancy_Queue<IP> and Simple_Queue<IP> where Fancy_Queue and Simple_Queue are derived from Queue, or implement the Queue interface.  But for polymorphic types, the actual parameters to the modules ("IP" in this case) must match. 

On the other hand, in a module instantiation, the rules are more flexible, and if the formal parameter to some module is "Queue<IP<>>" as in the Queuing_System module I suggested before, then the actual parameter in an instantiation of Queuing_System could be "Fancy_Queue<TCP>", meaning you could use a derivative of the Queue module, as well as a derivative of "IP".  In general compile-time instantiation, represented by module instantiation, is more flexible than run-time polymorphism (represented by "T+").  That is not particularly unusual in OOP languages that support both, but it would clearly be possible to make run-time polymorphism somewhat more flexible, but then you would be incurring run-time dispatch overhead in more places.  One of the goals of both ParaSail and Ada is to reduce the number of places where run-time dispatch overhead occurs, both for performance reasons, and for testing reasons.

Thank you.

Take care,

-Tuck

On Tuesday, April 23, 2019 at 2:55:02 AM UTC+7, Tucker Taft wrote:

On Mon, Apr 22, 2019 at 2:05 PM Zing Chen wrote:

...

Very clear. I have no question about this kind of covariance. But I'll take opportunity to re-formulate my previous question, in a simpler way. Let Queue<T> be a generic class describing a queue of T (the type of elements of the queue). Is there any relation between Queue<TCP> and Queue<IP>, two instances of Queue<T>, if type TCP extends (i.e. is derived from) type IP?

When you declare Queue, you have to specify something about "T."  You might want it to be merely Assignable, or perhaps Comparable or Hashable or Imageable.  E.g.:

    interface Queue<T is Comparable<>> is

       ...

    end interface Queue

At some later point, you could define another interface that required a Queue, and at that point, you could further constrain "T", so you could write:

    interface Queuing_System<Network_Q is Queue<T => IP<>>> is ...

by specifying some limitations on T in the formal type for Network_Q we limit what sort of Queue can be passed when instantiating Queuing_System.  Hence the following is an illegal instantiation of Queuing_System:

       type Simple_Queuing_System is

          Queuing_System<Network_Q => Queue<Integer>>  // Illegal

whereas this is a legal instantiation:

     type Better_Queuing_System is

         Queuing_System<Network_Q => Queue<TCP>>  // Legal

I hope that at least partially addresses your question.