In Grace, type Type is actually
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
- everything is more complicated
- we need the
forall declarator to introduce the variable S
- 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.
In Grace, type
Typeis actuallyWhy is this? This issue is my attempt to remind myself why.
Consider this definition for
Type:Notice that the result of the
&method — which is a type — is recorded in the comment, but not in the type ofmethod &(_)Giving
Typea type parameter lets us be explicit about this: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
foralldeclarator to introduce the variableSS & 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, sayNone, 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
Typehaving that type parameter. Maybe someone else can have a go at explaining it.