Short answer: “a type system centered on the use of set-theoretic types (unions, intersections, negations) that satisfy the commutativity and distributivity properties of the corresponding set-theoretic operations”.
Long answer, well, there are blog posts[0], the Design Principles of the Elixir Type System paper[1] and related presentations[2, 3, 4] that talk about it at length. Giuseppe Castagna’s site has many more related papers: https://www.irif.fr/~gc/topics.en.html
Sets and types are foundational mathematical concepts so I’m looking for how elixir’s types fit in that context. Union and intersection are not something that belongs only to sets.
It means that the types are built on unions, intersections, and negations[1]. It's a polymorphic type system with inference at the function level. It also does some type narrowing with pattern matching.
Unions, intersections and negations are available in types as well and are by no means exclusive to sets. The distinguishing feature of a set vs type is that a value belongs to just one type while it can belong to several sets.
Types do not inherently have any such restrictions. A value can belong to several types. In fact, if you posit types to have union, that necessarily follows.
I think they do, and as you mentioned you can explicitly remove such a restriction. Sets and types are once again two different kinds of objects in mathematical theory, and a set-theoretic type doesn’t seem to be based either on set theory or type theory.
If types have unions/intersections/negations, as you originally seemed to imply, then “a value belongs to just one type” is false (if x is of type A then it’s also of type A ∪ B for any B).
If they don’t unless you add them to “explicitly remove such a restriction”, then that means you’re making types more set-like (set-theoretic).
In strict “type theory”, it’s the latter: types don’t have unions (in the sense that set-theoretic types do). There are sum types, which are different.
I hear you loud and clear. And it is part fever dream that's slowly become real. So yah, just as you said it. For the LLM with the readmes, I will correct that best I can tonight(maybe tighter guided llm?) Or more of what I was thinking when I started this project.. how is the code though?
If we're talking about actual clean-room reverse engineering where only the overall design or spec is copied and not the specific code, then yes. In this process, one person would decompile the original and turn it into a human-readable spec, and another person would write their own implementation. But the decompiled code itself is never distributed.
That's very different from the decompilation projects being discussed here, which do distribute the decompiled code.
These decompilation projects do involve some creative choices, which means that the decompilation would likely be considered a derivative work, containing copyrightable elements from both the authors of the original binary and the authors of the decompilation project. This is similar to a human translation of a literary work. A derivative work does have its own copyright, but distributing a derivative work requires permission from the copyright holders of both the original and the derivative. So a decompilation project technically can set their own license, and thereby add additional restrictions, but they can't overwrite the original license. If there is no original license, the default is that you can't distribute at all.
In fact, the story of how Atari tried to circumvent the lockout chip on the original NES is a good example of this.
They had gotten surprisingly close to a complete decompilation, but then they tried to request a copy of the source code from the copyright office citing that they needed it as a result of ongoing unrelated litigation with Nintendo.
Yeah, I think it can. I'm reminded of the thing in the 80s when Compaq reverse engineered and reimplemented the IBM BIOS by having one team decompile it and write a spec which they handed to a separate team who built a new implementation based on the spec.
I expect that for games the more important piece will be the art assets - like how the Quake game engine was open source but you still needed to buy a copy of the game in order to use the textures.
Prima facie: what does std::move look like it's trying to band-aid fix? copy operations?
They expanded the Rule of 3 to the Rule of 5 for a reason. The operations work together. Move semantics simply work as an optimization when you know the data you're taking in won't be needed anymore and you can more or less "snatch" the data (to put it overly broadly). If you can't do that, you take a slow path and just copy properties one by one.
Garbage collection? Well, besides these languages not having that, managed languages are making the exact same decisions under the hood when optimizing. if it knows a reference is being assigned but then goes out of scope, it can do similar move semantics to save on a copy.
> Here, we consider the Finite Monkeys Theorem and look at the probability of a given string being typed by one of a finite number of monkeys within a finite time allocation consistent with estimates for the lifespan of our universe
Is it just being used as a marketing term?
reply