The package go/types, which can represent Go types, represents recursive types with cycles.
It also has explicit code to detect and handle such cycles when comparing types for identity, assignability, etc. Go compiler represents type with a different package, internal to Go compiler which is not importable by user code - but my guess is that it uses the same technique. On Tuesday, May 4, 2021 at 3:09:39 PM UTC+2 jesper.lou...@gmail.com wrote: > On Tue, May 4, 2021 at 1:16 AM Delta Echo <deltae...@gmail.com> wrote: > >> > Not sure what "handle" means in this case. >> >> I want to know how this is implemented. >> >> At some point in the compiler, you have type erasure, and you have an > untyped language. From there on, it's a function pointer / label. And you > allow for it to be nil, because the type is really a nil-able type[1]. At > this point, you don't have to worry about types: it already passed the type > checker so the program is sound. If you are interested in the type-level > implementation, the background is usually that of recursive types and their > treatment. That is the code will implement the theory of recursive types. > There are two overarching ways we currently know of which makes the system > sound: equi-recursion and iso-recursion. > > In the equirecursive scheme, you essentially take the limit (limes) of the > infinite rollout of the type and define that as the canonical > representation. You then "equi"-valize the types and make them all equal to > this limit-type, so they are the "same". It corresponds to having a cycle > in a representation graph, and you define running an "infinite amount of > times around the cycle" as your type. > > In the isorecursive scheme, the types are defined to be different but > "iso"-morphic, i.e., with the same structure. You have conversion > functions, usually called fold/unfold or roll/unroll to translate between > the different types, so we can "unroll" to the next isomorphic type as we > work through the recursion. It's kind of building the next cycle in the > graph on demand by asking for an unroll of the next cycle. > > To get there, when you have notation such as `type stateFn func(*Scanner) > stateFn` you treat the type identifier "stateFn" as a variable at the type > level, and detect it occurs inside the type definition body. The notation > you will see is μX. 1 + (*Scanner -> X). The mu is a binding site for the > X variable. it corresponds to a lambda in the lambda-calculus but at the > type level. The 1 is a representation of nil. + means "or". The arrow is a > function type from a *Scanner to an X. This makes it explicit what is going > on: either we are done, and return nil, or we have yet another state in the > state machine in which case it is represented as a function from a scanner > to X. > > To be honest, I haven't studied Go's recursive types enough to know if one > or the other of the above are being used. But it is very likely that one of > these schemes is used, perhaps in disguise. Many systems using > iso-recursion hide the roll/unroll functions inside other constructs of the > language, so the programmer doesn't have to explicitly work with the > isomorphism. As a general rule, the equi-recursive scheme tends to be > harder to work with, because the infinite expansion makes it hard to do > type inference and also invites algorithms to have infinite loops. > > Finally, if you want to pursue this to a larger extent, you will need > someone who treats it with more than a few paragraphs. Benjamin C. Pierce's > "Types and programming languages" spends an entire chapter on the above, > giving it proper treatment, formally. Searching for iso- and equi-recursion > also works, but note that people often take a lot of notation for granted > which means it could look like gibberish and bad handwriting (or as we tend > to say in Danish: feet of a crow --- it's not about eyes here). > > [1] Slight aside: modern compilers, that is any compiler using post ~2000 > architecture design will type all intermediate representations as well as > the assembly, only performing erasure just before machine code emission. By > typing intermediate languages, you obtain the extra power that you can type > check your optimizations, catching many errors early on. > > -- You received this message because you are subscribed to the Google Groups "golang-nuts" group. To unsubscribe from this group and stop receiving emails from it, send an email to golang-nuts+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/golang-nuts/114b8584-4ba3-4bdc-ac06-b5d95ab63eb5n%40googlegroups.com.
