Why typeintersect(Int8,Int16) == Union{}

General Usage
1

Doc:

While programs manipulate individual values, a type refers to a set of values.

By this, we can say that values come first, then types are created by grouping values. If so, typeintersect(Int8,Int16) should be Int8. Isn’t it?

2

No. The key is that Int8(5) is not the same value as Int16(5). They are equal to each other, but have different memory layout, call different functions and have different behavior.

2 Likes
3

IMHO, “memory layout” is not part of a value.

PS, Pascal’s definition of UInt8 (Byte): just a collection of integers.

type
  Byte = 0..255; // from help of Lazarus/FPC
4

To determine whether two values are identical, you have to use ===. Values that correspond to two different concrete types cannot be identical. For example,

struct Foo
    x::Int
end

struct Bar
    x::Int
end

julia> Foo(5) === Bar(5)
false

The same logic applies to Int8 and Int16:

julia> Int8(5) === Int16(5)
false
2 Likes
5

The reason memory layout is part of value is pragmatic. If I have 2 different values that take up different amounts of memory, a slot for one won’t be able to hold the other.

6

Basically, I would say this part of the doc is a simplification.
Good for someone first starting, but not so good once you start asking the hard questions like this.
Because it doesn’t refer to what particular reasons things might be in that set.
And you might think (reasonably) that two sets that are equal in value of elements would be the same type.

A more nuanced version of what that sentence is getting at can be found in Jeff’s thesis:

Our goal is to design a type system for describing method applicability, and (similarly) for
describing classes of values for which to specialize code. Set-theoretic types are a natural
basis for such a system. A set-theoretic type is a symbolic expression that denotes a set of
values. In our case, these correspond to the sets of values methods are intended to apply
to, or the sets of values supported by compiler-generated method specializations.

(emphasis mine)
Section 4.2 Type system (page 60)
Bezanson, J.W., 2015. Abstraction in technical computing (Doctoral dissertation, Massachusetts Institute of Technology).

So we can now say that typeintersect(Int8,Int16) should indeed be Union{},
because there is no set of values that dispatch or specialize in the same way as both Int8 and Int16.

3 Likes
7

Thanks.

Now I can study the lattice constructed on types.