You are of course right, but even if there was an opportunity for a major redesign, I am not sure this topic makes a compelling case for one — the software engineering problem is still unclear. Cf
Julia is sound—by which I assume you mean “consistent” since “sound” is a type system term whereas “consistent” is a logic term—because it exists in the real world. Any real system, even in a computer, by virtue of actually existing must be consistent. This is because reality itself is consistent: different accurate descriptions of reality must all agree with each other. (If you don’t believe this then we’ve got deeper problems than whether Julia’s modeling of types is consistent or not.) You can no more create a paradoxical object in Julia than you could build one in your living room. I cannot create a type in Julia which both contains and does not contain itself for the same reason I cannot make a single-color chair that is both blue and red: if you construct a type object in Julia, it exists, and you can just check if it contains itself or not, just as you can look at the chair and see which color it actually is.
It is only in the context of formal systems like Principia Mathematica that consistency even becomes a question in the first place because these systems are just a made up set of rules, and it’s not a given that they don’t produce contradictions. One way to look at the issue of consistency is that it is fundamentally about whether a collection of mechanical rules (i.e. a formal system) describe something which could potentially be “real”. The most basic way in which a formal system can fail to be realistic is if it is can produce contradictory statements about the reality it is supposed to describe. A formal system that allows a set that both contains itself and doesn’t contain itself at the same time, for example, cannot possibly describe anything “real” since in reality the set would either contain itself or not.
So asking about the consistency of Julia is the wrong question. Julia is guaranteed to be consistent because it exists. The question you should ask is whether the type system implemented in Julia can be mapped into a formalized set theory like ZF/C. We have every reason to believe that it can as long as you add non-well-founded sets to ZF/C (via any of the various anti-foundation axioms), which allows a type like Type which contains itself to be modeled. No one has proven this to be the case, but since the types which can be constructed in Julia are all finite, it’s pretty unlikely that anything really wild could possibly happen—there’s not a whole lot of controversy in the realm of finite sets.
2 Likes
Thanks for the long reply and the patience.
I really meant “unsound” in the sense of:
Does julia has no support for user defined non well founded sets because it would invalidate its type system otherwise?
@Tamas_Papp wrote:
I am not sure this topic makes a compelling case for one — the software engineering problem is still unclear.
The discussion with @StefanKarpinski was not about HKTs anymore and I’m sorry for this.
To implement true HKTs we would need the complete support of function types which will (never) be the case from what I heard about @yuyichao and @jeff.bezanson
Whereas abstractions over parametric sets, e.g C{_}, which is different than HKTs is possible, at least in my mind, but complicated due to runtime subtyping additional to parametric subtyping in julia.
I was toying with the following idea:
define <: (less than or equal for types) arbitrary and dynamically and possibly more than once … so that it would be possible to define something similar too:
abstract type AbsInt end
abstract type Abs2Int end
struct Foo
a::Int
end
set_ordering(Foo,AbsInt)
set_ordering(Foo,Abs2Int)
what are the drawbacks? or asking from a different direction, what are the benefits of having a single parent?
bar(::AbsInt) = 1
bar(::Abs2Int) = 2
1 Like
You might want to have a look at the lightweighted higher kinded types in Julia.
PDF is available here:
I have an article about this implementation coupled with type classes:
https://thautwarm.github.io/Site-32/PL/paper-reading-LHKP.html
1 Like
I have been reading ScalaFP: The Mystery of Scala's Higher-Kinded Types - DZone Java to understand higher kinded types. It looks Julia already has them
1 Like
Yea it’s kind of funny what you take for granted when you make Julia your lingua franca. I remember reading about Scala’s type system preparing for my last job and trying not to have my brain explode. Ironically, when I started writing Julia it just made sense… Like the idea of using a higher kinded type was a natural one, I didn’t need to read a reference or anything, just knew what I needed, typed it and voila it compiled.
Scala though… Scala can be a very scary language. Makes all the intuitive things sound like sorcery, simple code like hieroglyphs, logical patterns look like strange attractors… Not always, but anyone whose seen someone other then themselves write scala knows these things.
4 Likes
If thats what higher kinded types are I’d retract my previous post I just meant abstracted generic types in a hierarchy.