On Tue, May 4, 2021 at 1:16 AM Delta Echo <[email protected]> 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/golang-nuts/CAGrdgiXQo3zHEAgM8%2Bvn%3DzecN3GvajRN1ttKedPiSTJLO4jx2g%40mail.gmail.com.
