The transitivity failure linked above. Out of `x isa A`

or `!(x isa B)`

or `A<:B`

, which is the incorrect judgement? Or are we happy with lack of transitivity?

Then the way we almost have dependent types. Naively one would expect

```
julia> struct bi_inv{A,B} end
julia> is_isa = bi_inv{N,X} where Type{N}<:X<:Any where N
julia> is_int = bi_inv{N,X} where Type{N}<:X<:Int64 where N
julia> bi_inv{3, Int64}() isa is_isa
false #should be true
julia> bi_inv{3.5, Int64}() isa is_int
true #should be false
julia> Type{3} <: Int
true
julia> Type{3} <: Integer
false #transitivity fail
```

Then there are various front-end normalizations.

A proper documentation/spec would permit me to implement the julia type system: It would give me the necessary information to construct a data structure that is at least as expressive as julia’s type system, tell me how to map julia syntax into this data structure, and allow me to write code that does all the necessary judgements. Optimally this would allow a simple proof of transitivity / soundness, as well as a simple proof that judgements are decidable (algorithm must terminate in finite time), or even reason about computational complexity. The neccessary judgements are `isa`

, `<:`

and `is_concrete`

; the latter is absolutely essential because julia wants `A<:B && B<:A`

to imply `A==B`

, and wants this to imply `invariant{A} == invariant{B}`

and wants these to imply compatible data layouts. Cf the existential crisis segfault. (side-note: Since we need to judge concreteness of types anyway, why are we not exposing this to users?)

This information is missing; the only thing to do is to read the source. It is very hard to speak about “implementation bugs” since there is no spec.

The above may sound pretty devastating, but I am actually OK with julia’s type system being an informal and maybe unsound underbelly that is nevertheless pragmatic and very rarely touches real code.