Are there any plans to support higher order ranked types in julia?

Internals & Design
1

Higher ranked types is some form of higher order generics, but is not the same as higher kinded types (nested generics).
A typical situation occurs, if we want to apply a length function to a collection of heterogenous types. I will present it here in Haskell syntax.
The length function is itself polymorphic:

length::[T] -> int

Then we deine an apply function as:

apply::([T]->int)->([S],[R])->(int,int)

With ([S],[R]), we assume that apply take as its second argument a tuple with two elements which are may of different type S \ne R.
The apply function above would not compile as T do not have to be match S or R. In order to solve the problem above, we had to describe the type parameter T has higher order generic. Haskell do it by the forall keyword with

apply:: (forall T. [T]->int)->([S],[R])->(int,int)

Now, we have the guarantee that that our (higher order) type parameter T will match the type parameters S and R. The apply function is a rank-2 type (function) which is guaranteed to be decidable for type inference. For ranked higher order types with rank>2, the type inference becomes undecideable, but additional type annotations would help in certain cases.
I hope, that I have not done any mistake.

Are there any plans, at least for rank-2 types, to support this in Future?

Sources:
http://sleepomeno.github.io/blog/2014/02/12/Explaining-Haskell-RankNTypes-for-all/
https://www.stephanboyer.com/post/115/higher-rank-and-higher-kinded-types
https://wiki.haskell.org/Rank-N_types

2

Maybe you could translate this proposal to Julia for people who don’t understand the Haskell syntax? What problem would it solve in Julia?

3

Perhaps you this is useful reading: Proposal for a first-class dispatch wrapper

4

@nalimilan, sorry for this. AFAIK, function types are at momentum a hot topic and I did not know the final syntax for it, but I will try it with the synatx from
https://github.com/JuliaLang/julia/issues/210#issuecomment-35685282
Here is a suggestion:
function length{T}(Array{T})::int
function apply{R,S,T}(length::T->int,Pair{Array{S},Array{R}})::Pair{int,int}
function apply{R,S,forall T. }(length::T->int,Pair{Array{S},Array{R}})::Pair{int,int}

Edit: changed it to pair.
Edit 2: Wrap pair type parameters with Array{}

5

If I’m skimming and understanding that second link correctly, Julia already has far stronger support for higher rank and higher kindred types than Haskell: Haskell requires a language extension to use Rank-N types, while Julia is designed around dispatching with them. (I apologize in advance for any misrepresentation, I’m making generalizations off of skimming just one blog post summary, which I know is generally a bad idea.)

Also see previous discussions at Function Parameter Speculation #17168 - #28 by StefanKarpinski

6

Interesting side note: Stephan Boyer, who wrote the second post linked, is the number 30 contributor to the Julia repo in terms of commits. Most of that was a web UI for Julia written in C++ from long before Jupyter/IJulia was a thing. If anyone has ever wondered why there’s a “ui” directory just for Julia’s REPL code, it’s because there used to be web UI as well.

7

Damn, julia is so f?ck?ng powerfull!!!

The interesting point here is the type Type in julia. This is the higher order generic I’am searching for. The analogy of the type Type in julia is the similar for the class in java.
Each data type in julia is an instance of Type:

Int64 isa Type, Any isa Type, Array{Array{Int64}} isa Type
(true, true, true)

But each data type is not a subtype of type Type:

nt64 <: Type, Float64 <: Type, Array{Array{Int64}} <: Type
(false, false, false)

Why, because the type Type is a type of at least second order, where each data type in julia is of first order. The type DataType is exactly second order which can be proved by:

Int64 <: DataType
false
Type<:DataType
false

The type Type could be instance or a subtype of type Type:

Type isa Type # metaorder of the right type is one unit greater than the meta order of the left type
true
 Type <: Type #meta order is the same for the left and right type
true

The most powerfull type in julia is Any which is either a DataType or a Type (meta type)

Any isa DataType,Any isa Type
(true, true)

Back to my example:
Assume:

len{T<:DataType}(a: Array{T})::Int64=length(a)

Then, the apply below would fail (assume typed lambdas are available in julia) because only function with a concrete Type (DataType) could be used as parameter

apply{R,S,T<:DataType}(len::T-->Int64,p::Pair{Array{S},Array{R}})::Int64=len(p.first),len(p.second)

A solution would be:

apply{R,S,T<:Type}(len::T-->Int64,p::Pair{Array{S},Array{R}})::Int64=len(p.first),len(p.second)

because now a function len with a type parameter T could be used as parameter for apply.
The cool thing in Julia is opposite to haskell, that any unrestricted type parameter T in julia could not only be a DataType, but also a Type (MetaType), so this works to:

apply{R,S,T}(len::T-->Int64,p::Pair{Array{S},Array{R}})::Int64=len(p.first),len(p.second)

To specify that the type parameter T should only be type of meta order 2, we could restrict it by

apply{R,S,DataType<:T}(len::T-->Int64,p::Pair{Array{S},Array{R}})::Int64=len(p.first),len(p.second)

But here aroses a problem. How do we specify that a type parameter T is of order 3,4 or n. What we need is something like

apply{R,S,DataType isa X isa Y isa T}(len::T-->Int64,p::Pair{Array{S},Array{R}})::Int64=len(p.first),len(p.second)

which seems not to be allowed. Any suggestions?

Correct me, If I make a mistake.

8

What are you trying to accomplish here?

9

I play around with higher order generics.
One day, typed lambdas are supported, we can express to take parametric functions as argument, where the parametric parameter T has the meta order 2 (rank-2 type). Suppose we want to measure the length of different collection types T and we have a Pair p of different collections types

The length function can take collections with different collection types A as its first argument (assume for simplicity that the elements of the collections are all of the same type for all collection types ) by:

len{A}(a::A)=...

To apply the len function polymorph over the different collections in p (different in collection type), we defined the apply function as:

apply{R,S,T,T<:DataType}(len::T-->Int64,p::Pair{S,R})::Pair{Int64,Int64}=Pair(len(p.first),len(p.second))

which sould be the able to measure the length of p.first with len(a::A) if p.first isa coll1 and p.second with len(a::A) if p.second isa coll2. The apply function above takes a type parameter T of meta order 2 (aka rank-2 type), where T is bound to the type parameter A when calling apply.

We could further express it simplified with

apply{R,S,T}(len::T-->Int64,p::Pair{Array{S},Array{R}})::Pair{Int64,Int64}=Pair(len(p.first),len(p.second))

because the type parameter T could be itself polymophic, too. But here aroses the problem, that the Type parameter T could be of any meta order (aka rank). What if we say that the type parameter has the meta order three (rank three). A natural way would be to describe it by:

f{T,DataType isa T}(arg::T)=...

, but this is no valid syntax.
An alternative would be to specify the meta order of the type Type by Type{i}, where i is the meta order, such that:

Type{1} isa Type{2} isa Type{3}

should evaluate to true which is not the case as the expr Type{i} has another meaning in julia.
In the end, it would be usefull to constraint parametric types to a specific meta order or to a range of meta orders in order to support higher ranked types sufficiently.

10

No offense, but I think you need to stop thinking in Haskell here. In Julia, extreme polymorphism and genericity is the default, not something you need to jump through hoops to achieve. If you can explain in simple prose (without talking about types, ranks, higher orders or anything meta) what you want a function to do, perhaps someone can explain how to do it. It kind of sounds like you just want a len function that, when applied to a pair of collections returns the pair of their lengths? Is that correct? If so, then all you need to do is this:

julia> len(a::AbstractArray) = length(a)
len (generic function with 1 method)

julia> len(p::Pair) = len(p[1]) => len(p[2])
len (generic function with 2 methods)

julia> len([1,2,3])
3

julia> len([1,2,3] => ["foo", "bar"])
3 => 2
1 Like
11

@StefanKarpinski
What you presented above is subtype polymorphism, another way to sove the problem. The problem here, is not the len function , we can already express it (with intro of typed lambdas in future) with julia.
The problem is to restrict the

extreme polymorphism and genericity

of julia as needed by the user (narrowing genericity).
As an example, suppose we have a function

f{T}(x::T)=...

, the type parameter T could be of any genericity, allowing to call f with (Meta) Types which are to general in some cases.
As an example, I could imagine to model ontologies (like with OWL) in julia. In an ontology, you have classes and instances, where classes could be of any meta order.
For instance, a class of meta order one can only instantiates raw Instances, whereas a class of meta order 2 could instantiate classes of meta order one.
If I want to write a function f, which should only captures meta classes of order three as argument and throw otherwise an type error, I’ have to restrict the type parameter T to have only one meta order, namely three with
f{T,DataType isa T}(thing::T)=...
which is sadly not possible in julia.

I know that such a use case is very raw and the priority for such thing is very low, but the support of X isa Y constructs in the where clause of type parameters would complete the needs for ontology modeling and maybe for some other use cases.

12

Keep in mind that there is one big difference between Haskell and Julia:
Haskell is statically typed while Julia is dynamically typed so any typing errors will only be thrown at runtime not ahead of time at edit time (in an IDE with incremental compilation) or at compile time. So I don’t know if the sort of type restrictions you’re seeking are useful then since a runtime exception would accomplish the same thing.

1 Like
13

I’m having a little bit of a hard time decoding the meta talk, but it seems like what you’re asking for is being able to write an “is a” constraint like n::Integer in where clauses and type parameter declarations in addition to the “subtype of” constraints like T<:Real that we allow now? If so then sure, that is a desirable feature. However, not having this feature doesn’t limit the expressiveness of the language in any way. Sure, you can write nonsense types like Array{Int, Float64} or Array{:foo, 1.5}, but you can’t do anything with those types (like construct instances of them) so who cares?

2 Likes
14

@StefanKarpinski
Yes, this is what I want, an isa expression in the were clause. But, as I 've recognized, it does not really help if we cannot contruct types of a specific meta order.
This is not valid julia:

type Meta3{T, DataType isa T}
 thing::T 
end

Another useful extension of the were clause would be to restrict the type parameter to specific instances by:

p(a::T) where T in [Int64,Float64]

which could be equivalently done with union types:

f(x::Union{Int64, Float64})=x

which is, however, a bit clunky.

Edit: remove Type from it.

15

FWIW, you can check any computable constraint you want in an inner constructor, and thus guarantee that the combinations not satisfying this constraint never happen in practice (or signal an error immediately).

16

@Tamas_Papp
Did you mean something like that?

struct OrderedPair{T}
       x::T
       y::T
       OrderedPair{T}(x,y) where {T}= DataType isa T ? new(x,y) : error("hello")
end

It works, but I see here another problem:

julia> OrderedPair{DataType}(Int64,Float64)
OrderedPair{DataType}(Int64, Float64)

This should throw an error, the cause for this behaviour is:

julia> DataType isa DataType
True

which should be false in my eyes.
In the end, it seems that the support for isa in julia does not introduce any positive effect as meta levels are not implemented properly.

17

DataType is its own type:

julia> typeof(DataType)
DataType

so your code does what you asked it to do.

Possibly my fault, but I still don’t understand what you are trying to do, as in “solving a concrete problem”. A MWE would help.

18

I want some form of meta typing, initializing a type should create another type. It is, in my eyes, not possible in julia.

19

I think that your perspective comes from the ML family of programming languages. Informally, the agenda behind these can be summarized as “look, we can do (strong) static typing, without having having to write tons of type declarations (90% of the time)”. The constructs you are talking about make sense in that context.

Whereas in Julia, computations on the type system are not that interesting per se for the programmer 90% of the time, and are usually left to the compiler. The purpose of parametric types in Julia is to achieve efficient code generation for concrete types. That’s kind of the whole exercise: think of Julia as an extremely powerful DSL developed for this purpose. You may find this post and the replies useful:

When I started using Julia, I wanted the type system to be able to express various things. For example, I was awaiting triangular dispatch very eagerly, as a “must have” feature. Now that we have it, I find that I am not using it as much as anticipated (this does not mean it is not essential when needed).

If you are expecting Julia to do things which are on the frontiers for type theory, you will probably be disappointed. OTOH, if you want to invest in learning a language where the focus is on writing fast generic code, this is probably the right place.

4 Likes
20

See non-well-founded set theory for an extension of ZFC in which it is perfectly reasonable for a set to contain itself. (There are also category theoretic foundations of logic in which self-inclusion is coherent – topoi and all that.) Perhaps this is where the disconnect comes from: in Julia types are just normal values and there is no hierarchy of types in the Principia sense. Julia works much more like the original untyped lambda calculus. If you go looking for a hierarchy of higher order types, you’re not going to find it because it’s not there: DataType is its own meta type so the whole ranked type hierarchy collapses into a single level as it was in Frege’s original conception before Russell’s paradox tanked his naïve approach.

4 Likes