Why does Type type have a type parameter?

[apblack]

In Grace, type Type is actually

type Type⟦T⟧ = ...

Why is this? This issue is my attempt to remind myself why.

Consider this definition for Type:

type Type = interface {
    ... 
    &(other:Type) → Type
    // result is other & Self
    ...
}

Notice that the result of the & method — which is a type — is recorded in the comment, but not in the type of method &(_)

Giving Type a type parameter lets us be explicit about this:

type Type⟦T⟧ = interface {
    ... 
    &(other:Type⟦S⟧) → Type⟦S & T⟧ forall S
    ...
}

Here, the type argument of the result type of & tells not just us, but also the type-checker, what the result type actually is. The downside is that

1. everything is more complicated
2. we need the forall declarator to introduce the variable S
3. the result type is S & T, but that's only useful to the type checker if it already knows the meaning of &. And if the type checkwer already knows the meaning of &, then why is it so important to tell the type checker the meaning of &? To put it another way, if the & operation actually returned some other type, say None, then the above definition would still be correct.

Hence, I think that I've failed to convince myself that there is actually any benefit to type Type having that type parameter. Maybe someone else can have a go at explaining it.

[KimBruce]

I don't see the point, but perhaps James knows.

On Tue, Mar 7, 2023 at 10:49 PM Andrew Black @.***> wrote:

In Grace, type Type is actually

type Type⟦T⟧ = ...

Why is this? This issue is my attempt to remind myself why.

Consider this definition for Type:

type Type = interface { ... &(other:Type) → Type // result is other & Self ... }

Notice that the result of the & method — which is a type — is recorded in the comment, but not in the type of method &(_)

Giving Type a type parameter lets us be explicit about this:

type Type⟦T⟧ = interface { ... &(other:Type⟦S⟧) → Type⟦S & T⟧ forall S ... }

Here, the type argument of the result type of & tells not just us, but also the type-checker, what the result type actually is. The downside is that

1. everything is more complicated
2. we need the forall declarator to introduce the variable S
3. the result type is S & T, but that's only useful to the type checker if it already knows the meaning of &. And if the type checkwer already knows the meaning of &, then why is it so important to tell the type checker the meaning of &? To put it another way, if the & operation actually returned some other type, say None, then the above definition would still be correct.

Hence, I think that I've failed to convince myself that there is actually any benefit to type Type having that type parameter. Maybe someone else can have a go at explaining it.

— Reply to this email directly, view it on GitHub https://github.com/gracelang/language/issues/199, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAN2D6RF5MRMNHBRKV66QXDW3ATXHANCNFSM6AAAAAAVTMTSGA . You are receiving this because you are subscribed to this thread.Message ID: @.***>

-- Prof. Kim Bruce Computer Science Pomona College