Embedded types in types

[KimBruce]

[I know we have discussed this in the past, but don't remember why we made the following decision:] Currently we allow types to be defined in objects, but not in other types. This makes those embedded types nearly useless for static typing. Suppose for a moment that we allowed embedded types in types, as in T below:

type T = interface {
   type U = interface {   ???
       n -> String        ???
   }                      ???
   m -> U
}

def x:T = object {
   type U = interface {
       n -> String
   }
   method m -> U {...}
}

method r(y:T) -> Done {
    def z: y.U = y.m
   print (z)
}

The typing of method n makes perfectly good sense. However, if type T cannot contain the definition of type U, then r can't type-check because it doesn't know that y has (must have) an embedded type U, let alone guess what it is.

Moreover, how do we write the type of method m in T, when it depends on a U which does not occur otherwise in T.

This came up for us when type-checking imports. If we have an import statement:

import "im" as im

then we treat im as an object that contains all the public features of module "im.grace". Some of those are likely types. Suppose U is one such defined in im. In the importing program, we would write im.U to access the type U in im. The natural way to access this and other public features is to provide im with the type (call it $imModType) derived from the definitions in im. However $imModType cannot contain type definitions, so $imModType.U does not exist.

It gets even worse with public imports that are then accessible to yet other modules.

We can work around this by treating imported types differently from imported methods -- though it is quite awkward as im1.U logically should be looked up just like any other public component by looking at the type of im1 to see how it can be used.

Can someone tell me why we ruled this out? Was it just for simplicity or for some more substantive reason? I've had mixed feelings about including embedded types in either objects or types, but I found this situation fairly compelling.

[kjx]

I think the earlier version is at #124. I don't know how to merge the issues.

Given types are invariant over inheritance / conformance, and that we don't model ownership / nesting in the types (e.g. the U object can be inside any T object, not just the T in which that U is nested) then we probably don't need nested types at all. For a start, types probably have to be manifest and that will kill anything more exotic. We can just lift all types out to the top level of the module - I think this would work in that example.

Can someone tell me why we ruled this out? Was it just for simplicity or for some more substantive reason?

• types describe objects. so we said nested types must describe a slot in a confirming object that returns a metaobject represented a type nested inside that object.
• Or we could say that nested types establish nested types returned by the metaobjects. those type metaobjects have methods like match What if we try to write a nested type called match? (I guess we could just raise a not-declared-as-overloading error...
  • In more sophisticated systems (Tribal Ownership :-), where a : A, A.B and a.B' may not be the same type. (A.Bis the type of _any_ B object nested inside _any_ A object, whilea.Bis the type od a B object nested inside the objecta`). But again, since we're not making any of those distinctions, and are structural, can't all types can just go to the to level of the model. Alternatively, the typechecker could require all types only at the top level of the model...
• dot might know what the Right Thing is. Or Jilian Mackay's (Alex Potanin's student) on nested types in Wyvern...

I've had mixed feelings about including embedded types in either objects or types, but I found this situation fairly compelling.

well I like them too, but what we would have to do is work out what really is going on...

[apblack]

The conclusion of the prior discussion seems clear: read it here.

In the example that started this issue, the type of x is given by

type T = interface {
    U -> Type⟦interface { n -> String }⟧
    m -> U
}

[apblack]

It seems to me that this issue was resolved in 2020: no, types cannot be embedded in types.