Can types be declared inside methods (or blocks)?

[ghost]

Hopefully the title makes the issue clear. What consequences would allowing type declarations in inside of methods have and, the reverse, what consequences would banning them from inside of methods have?

[KimBruce]

Of course, if they are defined inside of methods, then they would have limited scope. Thus they could not appear in the types of any public methods, but they could appear in confidential methods. [On second thought, they might be able to appear, but they could not be visible in the type of an object that contains such a method. For example,

def o: {m: A -> U’,…} = object { type U = U’ & interface {…} method m(a:A) -> U’ {…} … }

It seems like that example should be legal as U extends U’.]

Because they are simply descriptive (structural), at first glance it seems like there would be no negative consequences (though I wouldn’t swear on it).

Kim

On Mar 19, 2018, at 7:51 PM, Richard Roberts notifications@github.com wrote:

Hopefully the title makes the issue clear. What consequences would allowing type declarations in inside of methods have and, the reverse, what consequences would banning them from inside of methods have?

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/gracelang/language/issues/164, or mute the thread https://github.com/notifications/unsubscribe-auth/ABuh-uTqEm43F1acZcrY8sfxYP9T2LDAks5tgG6TgaJpZM4SxNzU.

[kjx]

I don't see how that works at all. The question is which names are in scope where. For method signatures, they'll be names in external scopes plus any type parameters on the method.

[KimBruce]

OOPS! Sorry, long day. I was thinking about types inside objects, not methods.

If a type was defined in a method, it is only in scope inside that method. That’s still fine, e.g.,

method m(…) -> U { type T = {n: S -> U …} def o: T = object{ method n(s:S) -> V {…} … } def s: S = ... o.n(s) }

I don’t see any reason why that should be illegal. Obviously T should not escape the scope of the body of m, though of course you could define the same type (e.g., with a different name, e.g., T') outside of m and use that if, for example, if you wanted to return o.

I believe the only thing we don’t allow inside methods is other (direct) method definitions as we don’t know what to make of self in that case.

Kim

On Mar 19, 2018, at 11:21 PM, kjx notifications@github.com wrote:

I don't see how that works at all. The question is which names are in scope where. For method signatures, they'll be names in external scopes plus any type parameters on the method.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/gracelang/language/issues/164#issuecomment-374488840, or mute the thread https://github.com/notifications/unsubscribe-auth/ABuh-rzbwpLd2MeXUBjIeuBSbt4oVxtGks5tgJ_ngaJpZM4SxNzU.

[apblack]

I'm in the process of trying to implement types properly (in minigrace), which is forcing me to confront this question, and also the related question: can types be declared inside blocks?

What do I mean by "trying to implement types properly"? Right now (and since the earliest days of Michael's minigrace) they have been implemented like defs. This doesn't work, for two reasons:

1. Forward references to a type are undefined, like forward references to a def. This is because all of the types come into existence at the head of the scope, but are not initialized until later. Forward references need to work so that one can define a pair of mutually-recursive types.

2. If the type has type parameters, then there needs to be a way of re-evaluating the type when it is applied to various arguments. defs don't work like that.

My solution was to treat types like once methods. Because they are methods, they can have parameters, and can be evaluated several times for different argument values. Because they are once, they are initialized on demand, and recursion is not a problem, so long as it is well-founded. That is, a definition like

type A = A & B

will still lead to infinite regress, but a definition like

type A = interface { x -> A ; y(_:A) -> Self }

should be OK.

This works fine if the type definition is in an object (including a module): that object gets a additional method that returns a type. References to a type like A⟦Arg⟧ inside the object are treated as self.A⟦Arg⟧ in the usual way. References from the outside, obj.A⟦Arg⟧, work fine too.

However, if the type definition is in a method, there is no object to which to attach the type method. The same thing is probably true if the type definition is inside a block. In this case, we could perhaps give the block an extra method, but this seems weird, given that we can't declare any other kind of method inside a block.

If we did allow methods inside of blocks, then we would need another reserved word to refer to the block object itself, like thisblock. Or change the meaning of self inside a block, which I think would be a bad idea.

After kicking this around all evening (but not for longer than that); I've come to the conclusion that we can do without types in methods, just as we can do without methods in methods. The main usecase that I can think of is to allow the declaration of a local name for a type that is otherwise rather verbose. For example, in a method with type parameters K and V, one might want to define

type myDict = Dictionary⟦K,V⟧

to save some keystrokes. This is most likely to happen when the method is a class, in which case the type declaration can go inside the fresh object.

However, I'm aware that my position might stem from the difficulty of implementation, rather than a real language design problem. We could, as @kjx has frequently argued, do the full Self (and SIMULA) thing, and say that any activation record is an object, in which case methods could be objects, and blocks could be objects, and they could all contain methods (and types). How we refer to the different selfs is then a question of syntax. (What did Self do about that?)

What about types in types (#124)? I'm thinking that @kjx is right, and we should disallow the type syntax inside a type. Instead, we would give interface an additional method A

type typeWithNextedType = interface {
    meth (arg:X) -> Y
    A -> Type
}

[kjx]

On 15 Nov 2018, at 18:42, Andrew Black notifications@github.com wrote:

How we refer to the different selfs is then a question of syntax.

Self is aggressively flat - objects contain method slots contain blocks contain blocks and thats it. No further lexical nesting. That’s ‘for a reason, to support the direct manipulation interface.

[kjx]

I'm thinking that @kjx is right, and we should disallow the type syntax inside a type.

I’m right by definition :-)

If types are (once) methods - or at least are immutable so that we can’t tell how they are implemented - and it doesn’t make sense to have methods in methods., then it doesn’t make sense to have types in methods or types in types.

Instead, we would give interface an additional method A

I didn’t understand this.

J

[apblack]

@kjx writes

I didn’t understand this.

Sorry, I wasn't very clear. What I meant was, instead of writing

type GlobalType = interface {
    x → Number
    sum (_:B) → Number
}
type AnInterfaceWithANestedType = interface {
    m (n:Number) → Number 
    type B = GlobalType
}

we should write

type AnInterface1 = interface {
    m (n:Number) → Number 
    B  → Type
}

or, maybe, as you have suggested,

type AnInterface2 = interface {
    m (n:Number) → Number 
    B  → Type ⟦GlobalType⟧
}

if I'm understanding what you intended by the type parameter to the result type of the method that returns a type.

[kjx]

if I'm understanding what you intended by the type parameter to the result type of the method that returns a type.

yes and yes. That works well because types are shadows; we don't really want them to have a corporeal existence in programs.

if you think about typechecking something like this

def a : A = object { method m (n:Number) → Number {42} type B = GlobalType }

def b:a.B = globalObject.new

then, to typecheck the last line, we need to know the value of type a.B. Putting in the type parameter makes it explicit — otherwise the manifest rule (I guess) traces things back to the definition.

[apblack]

I edited your post to make it say what I think you meant! If I got it right, then I agree with you.

The point that I made in #124 was that adding a type parameter to Type makes sense only if it is used somewhere. There I proposed adding a method myType to type Type that returns the parameter — if we don 't do that, it can't be accessed, so it doesn't do any good.

[kjx]

can't be accessed, so it doesn't do any good

the entirety of static typing is based on type information that cannot be accessed...

[apblack]

the entirety of static typing is based on type information that cannot be accessed...

Well, yes. But I'm still not clear if that means we do or do not need a method in type Type⟦T⟧ that uses T.

I've updated the grammar and the spec to remove types from inside types and methods — see commit 191b803fe. (I also bumped the version umber to 0.8.1) There, I have given Type⟦T⟧ a method subject that returns T. If this is wrong, we should take it out.

More generally, please look at the changes in 191b803fe and make corrections as necessary.

[apblack]

I'm closing this issue, because we have decided that we are not going to allow types in types or in methods. (I don't think that they were ever allowed in blocks.)

The (somewhat separate) issue of whether type Type is parameterised, and if so, what the parameter means, is a also resolved, because no-one objected to the changes in the above-mentioned commit.