[Grace-core] Pondering types

[PSU via GMail]

I'm moving this to the Wiki.  Let's _not_ start another long email trail ....

https://projects.cecs.pdx.edu:8443/~black/NewOOL/index.cgi/wiki/TypesDiscussionKim

Andrew P Black

> On Mar 7, 2014, at 3:08, Kim Bruce <kim at cs.pomona.edu> wrote:
> 
> [A long post on some aspects of the type systems.  Comments/corrections/questions are welcome.  I find that writing things down helps me think about them, but discussions help clarify the ideas.]
> 
> Types in Grace
> 
> The following was inspired by my conversation with Tim (and Michael) about types in Grace.  Some we discussed in Wellington, but other parts are my further thoughts.  I’m focusing on static typing in Grace, but some parts (e.g., the introduction of SelfType) may have some impact on the core language as well.
> 
>  1.  Use of types defined as part of objects and/or classes:
> 
> 
> Types defined in objects are not actually parts of those objects, but instead are defined to have the object as their scope.  However, these type definitions are accessible outside of the object when qualified by the name of the object (e.g., type definitions are implicitly public).  There are a few consequences of this that I enumerate below.
> 
>  a.  Types defined in an object o do not show up in o’s type.  That is,
> 
> def o = object {
>    method m(a:T)->T{…}
>    def U = {n -> Number)
>    method p -> U {…}
> }
> 
> has type {m(a:T) -> T, p -> o.U}.  U does not appear on its own in the type of o, only in those places where it appears in the type of another definition or declaration.  As you can see from this example, sometimes the type of o will need to refer to a type defined inside it.  Thus it would be useful if we could write
> 
> type Tricky = {m(a:T) -> T, p -> o.U}
> def o:Tricky = object {
>    method m(a:T)->T{…}
>    type U = {n -> Number)
>    method p -> U {…}
> }
> 
> 
> This might be tricky to implement properly, but I don’t (at this time) see any theoretical barriers to allowing this. 
> 
> An alternative to the proposal not to include types in the types of objects would be to include the existence of U in the type of o, but not give further information about it:
> 
> type NotSoTricky = {
> 
>    m(a:T) -> T,
> 
> 
>    type U
> 
>    p -> o.U
> 
> }
> 
>  
> 
> Instead of writing type U we could write “U is Type” but I believe both are unambiguous with our current syntax.
> 
> I have somewhat mixed feelings about this last alternative.  It does give more information about the object (a good thing).  It also has some subtle consequences.
> 
> First, what are the consequences for subtyping?  If NST2 is a subtype of NotSoTricky, what do we need to know about its type U.  Can we check if it is the same as the U of NotSoTricky?  It doesn’t seem like it!
> 
> This seems to lead us off into something closer to a nominal or (worse) a dependent type system.  I think we would have to experiment with this a lot more before adopting it.  Thus I stick with the recommendation to just leave the types out. 
> 
> b.  Types defined in an object cannot be refined in an inheriting object.  This keeps us away from the complexities of languages like gBeta where types can be refined in subobjects (or a broken static type system like Eiffel’s).  The danger here is that one can break the typing of inherited code from the superobject.  All kinds of complications arise if this is allowed, so let’s just not allow it.  If we wanted to, we could allow putting a new definition of a type in a subobject that does not override the original, but just scopes it out (i.e., is treated as a definition that accidentally used the same name).  I’d prefer not to allow that (too confusing!), but it is a possibility.
> 
> c.  In order to have access to a type defined in another object, that object definition would have to be definitively static (is that the correct name?).  I.e., we would need access to the actual object definition and its type definition.  Otherwise we do not know for sure what the type definition is and cannot type check uses of the definition.
> 
> Essentially this means that we would need to have dereference either the object expression itself (which seems pretty weird) or, more likely, an identifier used in a definition of that object.  If o were an identifier that was a variable or parameter, then we couldn’t be sure what the actual definition was.  [Yes, we could do some static flow analysis to try to prove there was a unique definition of the type, but it doesn’t seem worth it.]
> 
> Definitions of the following forms:
> 
> 
> def o:U = object{…, type T = {…},…}
> 
> def o:U = myClass(…)  // myClass is a class definition
> 
> would certainly allow us to refer to olT (or o(…).T), but we could also allow the results of some other method calls if we desired (I’ll let others specify what is allowed).
> 
> 2. SelfType
> 
> I propose that we allow SelfType to occur as the return type of methods.  To make this more useful, I also propose that every object have a confidential parameterless method “shallowClone” that returns SelfType.  Without this it would be very difficult to define a regular clone method.
> 
> Introducing SelfType in this way, allows us to use it with cloning operations as well as with the style that Andrew has noted is popular with Smalltalk to allow cascading methods.  That is rather than defining a method to return Done, instead have it return SelfType as below:
> 
> method m(…) -> SelfType {
> 
>     some stuff
> 
>     self
> 
> }
> 
>  If method m above is part of object o which has static type T then o.m(…) will have type T.
> 
> 
> Notice that while SelfType is a subtype of the type consisting of all of the public methods of the object that contains it, it has no subtypes (except Bottom, if we have one).  That is because methods referring to SelfType can be inherited into objects that can have more public methods.  (More details on request.)
> 
> If we wanted to support binary methods (methods where the parameter type has to match the receiver type at run-time, i.e., methods with parameters with type SelfType), then we would also have to introduce exact types.  That would certainly give extra expressiveness, but I’m not sure it is necessary given our goals.  The basic idea is that an object expression has an exact type which includes all of its public methods.  A value has an exact type @T if it has type T, but not a subtype. 
> 
> If we do this, it might be better to treat SelfType as if it were an “exact” type.  That is, with most types, we say x:T means that at run-time, the type of the value associated with x is T or some subtype.  An advantage of having SelfType be exact, i.e., if x:SelfType then x has exactly all the public methods of the current object (no matter what the declared type, if any), then it limits the number of things that have SelfType and makes the actual use of SelfType easier.  This is essentially a proposal made by Na, Ryu, and Choe for adding a SelfType to Fortress 
> 
> 3.  Type parameters
> 
> Parameterized types will be written with all parameters to the left of the equals sign.  E.g.,
> 
> type BST<T> = {insert(n:T) -> Done, contains -> Boolean}
> 
> There is no need to express subtype constraints on parameter types in type definitions, though we could include them if desired.  However, we do sometimes need constraints when they are used as parameters in methods or class definitions.  E.g.,
> 
> class emptyBinarySearchTree<T> -> BST<T> where T extends Comparable<T> {…}
> 
> I’m not sure that “extends” is the best word for this.  The main justification is that it is what is used in Java.  However, I think words like “contains” or “includes” or something else might be better as “extends” isn’t very intuitive.
> 
>  4.  No wild card types
> 
> 
> Wild card types cause more pain that they are worth as they have complex restrictions that provide very limited advantages.  Moreover, most of the time they can be replaced by type parameters (details available if desired).  If we add exact types (see item 3) it might be reasonable to introduce named existentials, but I’d prefer to avoid them.
> 
> Kim
> 
> 
> 
> _______________________________________________
> Grace-core mailing list
> Grace-core at cecs.pdx.edu
> https://mailhost.cecs.pdx.edu/mailman/listinfo/grace-core
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mailhost.cecs.pdx.edu/pipermail/grace-core/attachments/20140307/78d8dc66/attachment.html>