Go Generics and Higher-Rank Types
517 views
Skip to first unread message
Aram Hăvărneanu
Aug 17, 2021, 11:20:28 AM8/17/21
to golang-dev
With generics, you can write a type like this:
type Foo[t any] t
But what happens when t is an interface type?
Go2go rejects it, although that seems to be an artefact of the
implementation rather than an explicit decision:
https://go2goplay.golang.org/p/LBdLLurworD
invalid receiver type instantiate୦୦Bar୦main୮aFooer
(instantiate୦୦Bar୦main୮aFooer is an interface type)
The gc implementation currently accepts the code, but it doesn't
behave as you'd expect (assuming you expect Bar to be a concrete
type). In particular, Bar.String seems unaccesible.
If it were accessible, through some simple identities[1] (equivalent
to De Morgan's laws), this would amount to higher-rank types[2].
Higher-rank types are very useful, in particular they allow one to
have polymorphic code operating on polymorphic values that can also
be serialized. Without Rank-2 types, you have to choose between
serialization XOR polymorphism.
Notice that this is somewhat related to Wadler's Expression Problem[3].
The Featherweight Go paper[4] provides a solution to the EP by
allowing Rank-2 polymormism on methods. If this were to be supported,
it would provide another solution to the EP.
However, since this particular aspect of Featherweight Go was
rejected (at least so far), it seeme likely that other sources of
higher-rank polymorphism are also supposed to be prevented, hence
this e-mail.
Should this work? How should this work?
If this is not supposed to work, then let this a reminder that if
higher-rank polymorphism on methods will ever be considered again,
this aspect also needs to be reconsidered.
[1] ∃a.P(a)
----------------- Remove-Exist
∀b.(∀a. P(a)→b)→b
[2] https://wiki.haskell.org/Rank-N_types
[3] https://homepages.inf.ed.ac.uk/wadler/papers/expression/expression.txt
[4] https://arxiv.org/abs/2005.11710
--
Aram Hăvărneanu
type Foo[t any] t
But what happens when t is an interface type?
Go2go rejects it, although that seems to be an artefact of the
implementation rather than an explicit decision:
https://go2goplay.golang.org/p/LBdLLurworD
invalid receiver type instantiate୦୦Bar୦main୮aFooer
(instantiate୦୦Bar୦main୮aFooer is an interface type)
The gc implementation currently accepts the code, but it doesn't
behave as you'd expect (assuming you expect Bar to be a concrete
type). In particular, Bar.String seems unaccesible.
If it were accessible, through some simple identities[1] (equivalent
to De Morgan's laws), this would amount to higher-rank types[2].
Higher-rank types are very useful, in particular they allow one to
have polymorphic code operating on polymorphic values that can also
be serialized. Without Rank-2 types, you have to choose between
serialization XOR polymorphism.
Notice that this is somewhat related to Wadler's Expression Problem[3].
The Featherweight Go paper[4] provides a solution to the EP by
allowing Rank-2 polymormism on methods. If this were to be supported,
it would provide another solution to the EP.
However, since this particular aspect of Featherweight Go was
rejected (at least so far), it seeme likely that other sources of
higher-rank polymorphism are also supposed to be prevented, hence
this e-mail.
Should this work? How should this work?
If this is not supposed to work, then let this a reminder that if
higher-rank polymorphism on methods will ever be considered again,
this aspect also needs to be reconsidered.
[1] ∃a.P(a)
----------------- Remove-Exist
∀b.(∀a. P(a)→b)→b
[2] https://wiki.haskell.org/Rank-N_types
[3] https://homepages.inf.ed.ac.uk/wadler/papers/expression/expression.txt
[4] https://arxiv.org/abs/2005.11710
--
Aram Hăvărneanu
Ian Lance Taylor
Aug 17, 2021, 3:17:47 PM8/17/21
to Aram Hăvărneanu, golang-dev
type Bar[t any] t
it seems clear that Bar[t] should look and behave like a t. When you
write Bar[Fooer] using the interface type Fooer, what you get is a
value of interface type. That value will have some dynamic type and a
value of that dynamic type. When you convert a value of interface
type to interface{}, for example by passing it to fmt.Printf, you pass
that dynamic type and value. The fact that the value was once a
Bar[Fooer] is lost. And so the fact that there is a String method
defined on Bar[t] is lost.
I'm not sure what the right resolution is here.
Ian
Matthew Dempsky
Aug 17, 2021, 4:03:29 PM8/17/21
to Ian Lance Taylor, Aram Hăvărneanu, golang-dev
Seems like another argument for golang.org/issue/45639.
--
You received this message because you are subscribed to the Google Groups "golang-dev" group.
To unsubscribe from this group and stop receiving emails from it, send an email to golang-dev+...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/golang-dev/CAOyqgcVAR7Cp50gyOwKDdJnLJCcK4u8qxRp0sd14-E%3DEuLVANQ%40mail.gmail.com.
Aram Hăvărneanu
Aug 17, 2021, 4:49:00 PM8/17/21
to Matthew Dempsky, Ian Lance Taylor, golang-dev
One thing to mention that I have never seen mentioned or discussed
in the context of Go generics is that Go is special in that it has
first class existential types (interfaces). *Every* other language
with generics is different. They start with parametric polymorphism
(viz. universal qualifier in Curry–Howard correspondence), and
introduce existential types using rules akin to De Morgan's in
classical logic (not 100% correct in constructive logic, but true
enough as an intuition in this discussion, and true in Go, as Go
terms inhabit a finite universe of types (again different from
languages based on System Fω)).
But we *start* with existential types, we already had interfaces,
and we already had higher-rank polymorphism, even though we didn't
have type constructors! Higher-rank polymorphism is a feature Go
already has, today, even before introducing generics, it's just
expressed in a very different way compared to languages based on
System Fω, but it has to be intrinsic to any semantic formalization.
Of course, existentials are dual to universals. And just as we can
encode existentials as universals in languages without "native",
"syntactic" existentials, we can do the reverse (baring technical
nitpicks that arise from the difference between classical and
constructive logic, which as I already mentioned do not concern Go,
whose programs' terms only inhabit finite monomorphic types).
Before generics, Go could treat existentials as types different
from other types. Without type constructors, there wasn't any way
to algebraically transform an existential into anything else. Indeed,
this is (one of) the reason(s) why type assertions in Go can't be
statically-checked.
However, with generics, now we have universally-qualified type
constructors and the full power of logic that comes with it. And
this mathematical logic tells us that existentials can't be separated
from universals. Something's gotta give.
Introducing some kind of restriction on universals means breaking
the Curry–Howard isomorphism. It would also mean that universals
will be able to express less things than existentials, which seems
backwards. It also implies some lack of orthogonality somewhere.
It would be a total shame.
I don't think we need to abandon CH. Before type constructors, we
didn't need to concern ourselves with kind-safety[1] because our
types were kind-safe by construction. Interfaces are indeed separate
from concrete types, and that's a distinction of kind that has to
be preserved in the semantics.
(As an aside, the reason we could achieve so much without generics,
is exactly because they can express higher-rank polymorphism,
something that other languages without generics can't do.)
[1] https://en.wikipedia.org/wiki/Kind_(type_theory)
--
Aram Hăvărneanu
in the context of Go generics is that Go is special in that it has
first class existential types (interfaces). *Every* other language
with generics is different. They start with parametric polymorphism
(viz. universal qualifier in Curry–Howard correspondence), and
introduce existential types using rules akin to De Morgan's in
classical logic (not 100% correct in constructive logic, but true
enough as an intuition in this discussion, and true in Go, as Go
terms inhabit a finite universe of types (again different from
languages based on System Fω)).
But we *start* with existential types, we already had interfaces,
and we already had higher-rank polymorphism, even though we didn't
have type constructors! Higher-rank polymorphism is a feature Go
already has, today, even before introducing generics, it's just
expressed in a very different way compared to languages based on
System Fω, but it has to be intrinsic to any semantic formalization.
Of course, existentials are dual to universals. And just as we can
encode existentials as universals in languages without "native",
"syntactic" existentials, we can do the reverse (baring technical
nitpicks that arise from the difference between classical and
constructive logic, which as I already mentioned do not concern Go,
whose programs' terms only inhabit finite monomorphic types).
Before generics, Go could treat existentials as types different
from other types. Without type constructors, there wasn't any way
to algebraically transform an existential into anything else. Indeed,
this is (one of) the reason(s) why type assertions in Go can't be
statically-checked.
However, with generics, now we have universally-qualified type
constructors and the full power of logic that comes with it. And
this mathematical logic tells us that existentials can't be separated
from universals. Something's gotta give.
Introducing some kind of restriction on universals means breaking
the Curry–Howard isomorphism. It would also mean that universals
will be able to express less things than existentials, which seems
backwards. It also implies some lack of orthogonality somewhere.
It would be a total shame.
I don't think we need to abandon CH. Before type constructors, we
didn't need to concern ourselves with kind-safety[1] because our
types were kind-safe by construction. Interfaces are indeed separate
from concrete types, and that's a distinction of kind that has to
be preserved in the semantics.
(As an aside, the reason we could achieve so much without generics,
is exactly because they can express higher-rank polymorphism,
something that other languages without generics can't do.)
[1] https://en.wikipedia.org/wiki/Kind_(type_theory)
--
Aram Hăvărneanu
Robert Griesemer
Aug 22, 2021, 7:48:24 PM8/22/21
to Aram Hăvărneanu, golang-dev
Thanks for this. We are aware of this issue. We may end up disallowing
it for now.
- gri
it for now.
- gri
> --
> You received this message because you are subscribed to the Google Groups "golang-dev" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to golang-dev+...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/golang-dev/CAEAzY39XDGj6tQhm_zzjX-M8Z-_W_usFq_Gz%3DbgJqd_uRUs88g%40mail.gmail.com.
> You received this message because you are subscribed to the Google Groups "golang-dev" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to golang-dev+...@googlegroups.com.
Reply all
Reply to author
Forward
0 new messages