[Grace-core] Modules & Inheritance

[Kim Bruce]

Yes on typos (thanks!), and yes, I am suggesting the more restrictive version as that makes type checking easy and shouldn't cause any issues with our intended set of applications for novices.

Kim



On Oct 19, 2012, at 3:05 PM, Andrew P. Black wrote:

> 
> On 18 Oct 2012, at 22:15 , Kim Bruce wrote:
> 
>> It occurred to me tonight as I was navigating the LA freeways that the simplest solution is to have the associated type include the full definition.  That is the type of o1 below would be
>> def T{type t = {a... b..., m: ...}
> 
> I think that you meant to write 
> 
> 	type  T = {type t = {a... b...}, m: ...}
> 
>> That is type definitions don't just have type "type", they must exhibit the full type definition.  Thus the types of o1 and o2 would be different, and anything of type T must have t = {a... b..., m: ...}
> 
> Again, I think that you mean t = {a... b...} 
>> 
>> 
>> Kim
> 
> Yes, that's just what I was saying.   Note that, although the types of o1 and o2 would be different from each other, they might both conform to type T:
> 
> 
> def T = {type t = {a ... b ... } , m:...}
> 
> def o1 = object {
>                  type t = {a ... b...}
>                  method m ....
>             }
> 
> def o2 = object {
>                  type t = {a ... e...}
>                  method m ....
>             }
> 
> 
> Then, when one refers to o2.t in a type context, we know that we need a manifest type, and that's T.t
> 
> In my previous email I was saying that, if o has type T, and T.t is a type, then o.t must also be a type such that o.t conforms to T.t
> I can see that this creates some type-checking issues when o2.t is used in a negative (contravariant) context.  Suppose that o2's method m takes an argument of type o2.t .   Giving it an argument of type T.t may not be good enough, because the body of m might request method e on that argument.
> 
> The alternative — and perhaps this is what you are saying — is that if o has type T, and T.t is a type, then o.t must also be a type such that o.t = T.t.   This is obviously a lot more restrictive, but the type-checking issues go away.
> 
> 	Andrew
> 
> 
> 	Andrew