Remove remnants of bytecode interpreter (or, alternatively, fix it)

[c3d]

The bytecode interpreter (-O1 option) is entirely broken.

Choose one of the following options:

1. Get rid of it entirely (which is a problem because of opcodes, which contains al the automation for bytecode
2. Fix it, make it type-safe and faster than the interpreter.
3. Redesign it to emit opcodes as text, much like the old XL2 bytecode

[dumblob]

Newbie here. I've just read the XL history and I'm still a bit confused about state of things regarding compilation with static types to a native binary. Because XL is so versatile, there can be (from what I understand) apps written in a way which does require runtime "eval" (e.g. through bytecode interpretation). There can be also apps written in a way which can be fully compiled to a native binary without any runtime "eval" and without garbage collector. And of course apps which can combine both (but I'm not sure whether XL "toolchain" does support such compilation).

Am I right about this understanding?

[c3d]

On 10 Jun 2021, at 21:21, dumblob ***@***.***> wrote: Newbie here. I've just read the XL history and I'm still a bit confused about state of things regarding compilation with static types to a native binary. Because XL is so versatile, there can be (from what I understand) apps written in a way which does require runtime "eval" (e.g. through bytecode interpretation). There can be also apps written in a way which can be fully compiled to a native binary without any runtime "eval" and without garbage collector. And of course apps which can combine both (but I'm not sure whether XL "toolchain" does support such compilation). Am I right about this understanding?

You are right about the theoretical understanding. However, there was never a fully functional implementation that worked without garbage collection. I never completed a type inference that was solid enough. It took me a while to understand why I was running into problem, until I reduced it to the fact that XL as currently defined accepts the following type: type goedel is (X: not goedel) In other words, something belongs to the goedel type if it does not belong to the goedel type. I am still trying to figure out what is the minimum set of rules that allows me to deal with cases like this correctly. An option would be to remove not. There are other ideas. None I like.

…

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#37 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAM6BNCE34YEDJHBF3FQZPDTSEGDHANCNFSM4KSCXCSA>.

[dumblob]

Ok, I understand.

...An option would be to remove not. There are other ideas. None I like.

Could you point me to those ideas?

Generally it'll need to be some trade-off. I wouldn't like any "one solution rules them all" approach (like the "remove not"). But I'd say some of the state space can be covered with higher-level rules with higher precedence (new "axioms" - maybe tens or hundreds of them) and the rest will be an error (i.e. let the user decide).

I myself don't care the language is undecidable, I just need it compile the code to HW-executable binary 😉. For decidability etc. there are special tools like Kind.

[PROMETHIA-27]

I would intuitively think a contradictory definition like above would simply equate goedel to something like the "never"/! type in rust; a type to which no value belongs. I guess that's sort of like nil in current XL? I'm unsure whether nil is more like null/None, void/()/Unit, or Never. null/None being "there could be something, but there isn't", void/()/Unit being a valid value that carries 0 bits of information, and Never/! being an unconstructible type (also defined as a sum type with 0 variants). Or maybe it's all of the above?

Would just saying "goedel is a type for which no value exists" be correct/usable? In rust such types are used to represent the return value of expressions that do not ever return, such as panic!, abort, exit, or a truly infinite loop. I think such a type could also be called "bottom" or ⊥, but I'm not entirely familiar with the more mathematical definitions of things.

I'd think the only major difference would be "there happens to not be a matching value for this type" vs "there can never exist a value that fulfills this definition", so that a type type mammal is (D: animal and furry) where nothing happens to exist that is both animal and furry doesn't get counted as being an empty type.

[c3d]

I would intuitively think a contradictory definition like above would simply equate goedel to something like the "never"/! type in rust; a type to which no value belongs.

Not really: it's a type for which I cannot decide anything at compile time, and would run into an infinite loop if I checked it at runtime. It is the type system equivalent of a definition like X is not X. You can compute it at runtime, but it will flip forever, and you cannot compute it at compile time. The original type inference algorithms do not have the notion of a type you cannot evaluate at compile-time, and I did not know I needed that capability until I ran into that problem.

I guess that's sort of like nil in current XL? I'm unsure whether nil is more like null/None, void/()/Unit, or Never. null/None being "there could be something, but there isn't", void/()/Unit being a valid value that carries 0 bits of information, and Never/! being an unconstructible type (also defined as a sum type with 0 variants). Or maybe it's all of the above?

The XL nil at the moment is more like "there could be something but there isn't". However, in that same vein, that is also the type for the return value when you don't need a type. It is also a type with no value other than nil, but you can create an infinity of such types. You can create a void type if you want, it's nothing more special than an empty struct in C.

Would just saying "goedel is a type for which no value exists" be correct/usable?

I don't think so. I think it's more like goedel is a type for which the question whether a value belongs to the type is not decidable.

In theory, with the current definition, you could create in XL a valid_url type which only accepts values for which the URL can be fetched and does not return, say, a 404. I'm using this example just to show a more extreme case of a type that cannot be decided at compile-time. Now, I'm seriously pausing here to figure out if such types make sense to allow at all, or if I restrict the language to say: "whether a value belongs to a type has to be decidable at compile-time".

In rust such types are used to represent the return value of expressions that do not ever return, such as panic!, abort, exit, or a truly infinite loop. I think such a type could also be called "bottom" or ⊥, but I'm not entirely familiar with the more mathematical definitions of things.

Yes, the type for "unreacheable code" for example is a slightly (if related) problem. However, that one is decidable at compile time. As a matter of fact, it primarily exists to allow the compiler to optimize away stuff at compile-time when it's known by the developer that a case cannot exist.

I'd think the only major difference would be "there happens to not be a matching value for this type" vs "there can never exist a value that fulfills this definition", so that a type type mammal is (D: animal and furry) where nothing happens to exist that is both animal and furry doesn't get counted as being an empty type.

A difference in terms of implementation is whether I can use that to actually generate better code.