Are there any (long term) plans to add higher order generics (a.k.a. higher kinded types) to Julia?

question

#21

I don’t think the recent type system changes provide higher-order generics exactly. I believe https://github.com/JuliaLang/julia/issues/18466 captures what something like this feature would look like in julia. E.g. you could define

type Compose{C1, C2, T}
    data::C1{C2{T}}
end

Julia doesn’t really have a kind system in the usual sense. The type system does not classify types according to what parameters they are able to accept. Indeed it does not model “type application” at all; that only takes place as part of execution (semantically of course). The type system only sees “fully formed” types, and has very little idea how they got that way. So it’s not the case that Vector{Int} is a type and Vector is a type constructor. Rather they are both just types, the latter being less specific. The fact that Vector can be applied to a parameter with { } is worked out at run time based on its representation. In theory, you can have a type equal to Vector that cannot be applied to a parameter, for example Union{Vector, Vector}.

We typically get around the lack of e.g. a kind system by saying, if you need anything fancier, just use normal functions! For example

compose(C1, C2, T) = C1{C2{T}}

or other things like the eltype or promote_type functions. These are obviously Turing complete, so if you can’t do what you want it’s rather suspicious :slight_smile: The remaining debate is then only about which things must be types, vs. which things are arbitrary expressions that get evaluated at some point. In the case of #18466, currently field types need to be types but we could relax that and allow them to be expressions.


#22

Currently field types can be expressions, as long as they don’t use any typevars (since they are evaluated when the parameterized type is defined, instead of when the typevars are all bound to create a concrete type).
This was the issue I’d brought to your attention on the last day of JuliaCon 2016.
Solving that would make a very big difference in making “clean” types (that don’t have to have extra parameters visible that were added to work around this), for example for a numeric type that is parameterized by the precision in bits, but needs to calculate the number of limbs for a field limbs::NTuple{N,UInt}, for example.


#23
type Compose{C1, C2, T}
    data::C1{C2{T}}
end

It would be nice if such a construct will come into julia.
Is it also planned some day to allow some day definitions like that:

function f(x::T1{T2{T3}}) where {T1<:...,T2<:...,T3<:...}

Of course we can construct types by:

compose(t1::Type,t2::Type,t3::Type)=t1{t2{t3}}

But how do we constrain a function to take only doubly nested Type:

fun(x::Type{Type{Type}})=x

which does not work when call:

fun(((1,),))

as we have to put the type of ((1,),) into fun, but even this does not work as

gun(x::Type{Type{Type}})=x
gun (generic function with 1 method)

julia> p=typeof(((1,),))
Tuple{Tuple{Int64}}

julia> gun(p)
ERROR: MethodError: no method matching gun(::Type{Tuple{Tuple{Int64}}})
Closest candidates are:
  gun(::Type{Type{Type}}) at REPL[125]:1
Stacktrace:
 [1] macro expansion at ./REPL.jl:97 [inlined]
 [2] (::Base.REPL.##1#2{Base.REPL.REPLBackend})() at ./event.jl:73

because of the fact that Tuple{Tuple{Int64}} isa Type{Type{Type}} is false.


#24

A possible solution to support HKTs could be provided by a new Meta Type, e.g. NestedType
The Type NestedType is parametrized by two integer, the first one describing the minimum, the latter the maximum nesting depth
In detail:

Int64 isa NestedType
=> false
Tuple{Int64} isa NestedType
=> true
Tuple{Tuple{Int64},Int64} isa NestedType
=>true
Tuple{Tuple{Int64},Int64} isa NestedType{1,N} where N
=>true
Tuple{Tuple{Int64},Int64} isa NestedType{1,1}
=>false
Tuple{Tuple{Int64},Int64} isa NestedType{1,2}
=>true
Tuple{Tuple{Float64},Tuple{Float64}} isa NestedType{2,2}
=>true
#Tuple{Any}=>isa NestedType, NestedType{M, N} where {M,N}
#Tuple{Tuple}=>isa NestedType, NestedType{M, N} where {M,N}

Every time an generic type is declared by:

struct type{T,S,...} <: ...
    ...
end

the generic struct type is implicitly treated as an instance of NestedType{M,N} where {M,N}.
A non generic struct type is like primitive types a FlatType

If a generic struct type t is instantiated, the minimum and maximum nesting depth is determined by:
min_depth(t),max_depth(t)=min(min_depth(T1),min_depth(T2),…)+1,max(max_depth(T1),max_depth(T2),…)+1
where the generic type t is parametrized by T1,T2,…
and min_depth and max_depth of flat types are zero.

A function definition like:

f(x::S{T}) where {S,T}

is then a syntactic sugar for:

f(x::V) where {V isa NestedType{1,N} where N}

#25

It’s still quite unclear to me what problem you’re trying to solve here. It seems like you’re going to great lengths to shoehorn a Principia Mathematica style hierarchy into Julia for its own sake. But Russell and Whitehead didn’t want a hierarchy of types in the first place, they only added it to their logical system to avoid the construction of paradoxical sets. We don’t have that issue, so what problem does this rather complex proposal solve? As far as I can tell, allowing type parameters to be used in more places does not require stratifying Julia’s type system.


#26

No, it is not the same as in Higher Ranked Types.
What I want here is to support Higher kinded types (Nested generics).

We can as Jeff said construct types already by

compose(a::Type,b::Type,c::Type)=a{b{c}}

but how do we type check such a nested type in a function?
This here do not work:

f(thing::Type{Type{Type}})=...

With the NestedType, which is probably not a Meta Type as I see yet
you could say equivalently:

f(thing::S{T{R}}) where {S,T,R}=...

which rewrites to:

f(thing::V) where {V isa NestedType{2,N} where N}=...

#27

We don’t – we run the code and see if it works. The only thing Julia needs in the type system is the ability to dispatch on such a type, not type check it. It doesn’t seem like this NestedType{2,N} idea helps with expressing dispatch – it appears to throw away too much information.


#28

Ok, then dispatching.
Which information is thrown out?


#29

The fact that a given type contains nested type parameters isn’t inherently informative. What it means depends upon the outer type. For example:

struct ArrayOfVectorsOfInt{N} <: AbstractArray{Array{Int, 1}, N}
    # …

So, now, is that type a 2-nested type? Or a 1-nested type? You can dispatch on either ::ArrayOfVectorsOfInt{1} or ::AbstractArray{Array{Int,1},1}. Instances of this type are (isa) both.

You really cannot say anything meaningful about what T{S{R}} means without knowing what both T and S are.


#30

Yes, this make sense.
I’ve think about it a bit more. A big problem to me seems not only inheritance but rather the extreme genericity of julia.
Is it ever decidable to determine the correct nesting of polymorphic types?


#31

There is some discussion about decidability in chapter 4 of Jeff’s thesis: https://github.com/JeffBezanson/phdthesis


#32

Sorry for pinching you guys, but I have another idea.

It would not solve the dispatching problem, but would make Higher Kinded Type construction more safely.
One problem is that:
f(a,b,c)=a{b{c}}
permit a and b to be of any kind. But what we want is that a,b are UnionAlls, i.e. can be specified with type parameters. Something like that would be nice:

f(a::UnionAll{T},b::T,c::S) where {S,T<:UnionAll{S}}=...

If at someday interfaces/traits are supported, we could express that something abstract adds a element to it of the type of the other elements in it by:

f(a::S,b::T) where {S<:UnionAll{T},S implements addto,T}=(addto(a,b);return a)

To allow such constructs, the type of existing things like:

typeof(Tuple)=>DataType

have to be changed to:

typeof(Tuple)=>UnionAll{T,N} where N<:Int64

In difference to the current handling is that a method not found error can be thrown instead of a Type{} … Error which is better for packages that contain no source code anymore.

What do you think of?


#33

But Russell and Whitehead didn’t want a hierarchy of types in the first place, they only added it to their logical system to avoid the construction of paradoxical sets.
We don’t have that issue,

I don’t believe you, how you would construct a set in julia which contains all types which do not include themselves (Russel’s paradox)?

The only thing Julia needs in the type system is the ability to dispatch on such a type, not type check it

It should be possible, but to which price is another issue.
For instance you have the following function:

f(i::C1{C2{C3}}})=f(i::C1{C2{C3 where C3} where C2}) where C1

Then you have a partial order C1->C2->C3, C1 constrains the set of acceptable type tuples of f much more than C2 and C2 much more than C3 because of the following relationship:

temp

If you instead have something like that:

f(i::C1{C2{C3}}) where {C1,C2,C3}

then, all paremeters constrain f equally but because C1 and C2 have the constraint to be a parametric set/unionall type there will not so many choices for them as for C3, so bounding C3 will shrink f’s size much more than for C1,C2.

You will get many ambiguities for the latter case as for any other multi generic function:

fun(a::S,b::T)=...
fun(a::Int,b::T)=...
fun(a::S, b::Float)=...
fun(1::Int, 2.0::Float)=?

There are also other cases for C1{C2{C3}} where some of the params get bound in deeper layers than others in which the deepness degree has to be respected.


#34

Unlike Russel’s sets, Julia objects are finite and constructed over time. If you collect all non-self-containing sets in Julia and take a union of them to make a type containing all of them, you always get a new type which doesn’t contain itself since it didn’t exist when you collected the types. So you can never create a Russel’s paradox type, only a chain of bigger and bigger types each containing all the previous ones but not themselves.


#35

To recapitulate the intention, a Type inside a Type is a different set but which shares the same name.


#36

I have no idea what that means…


#37

I have no idea what that means…

Either, the set “Type” in julia does include itself, then it is a non well founded set but have to be infinite which is contradictory to the statements that all sets/objects in julia are finite

Or , the set “Type” contains a set “Type” which is different because it was constructed before, but then two different sets share the same name which is contradictory.


#38

Non-well-founded sets need not be infinite.


#39

Non-well-founded sets need not be infinite.

Sorry okay, infinite regression means not infinite.

So, the reason why julia is sound is that it has pre-defined non well founded sets, e.g. Type, DataType,
but it doesn’t allow to define custom non well founded sets and therefore excludes Russel’s paradox.

Do you agree with this?


#40

Hi. I just want to point out that Julia is in the home stretch of the version 0.7 release, meaning there is a lot detailed wrap-up work going on and probably not a lot of room in the short term for fundamental rethinking.