make Method objects callable (and inferred) as invoke

[quinnj]

I don't pretend to understand the full set of ramifications of something like this, but am interested in opening a discussion and at least hearing from others. The idea is:

Function

would become

Function{A,R}

where A would be a Tuple{T...} representing a function's argument types, and R would represent the return types T or Tuple{T...}.

It would then follow that the function:

f(x::Int) = Float64(x * 2)

would have the type of:

julia> typeof(f)
#f{Tuple{Int},Float64}

I could see some very useful scenarios for this, such as the "date adjuster" functions in Base, which explicitly require any function that returns a Bool; this could then be defined like:

adjust{A}(f::Function{A,Bool}, ...)

Anyway, I know there are other type system improvements in the works, and wanted to throw this in the ring in case it meshed well with other changes.

[JeffBezanson]

See also: #17162 #210 #16191

The most obvious problem is what to do when f has more than one method.

I think we could have a type like this, for when you want to opt-in to characterizing a function by its argument and return types. However it should probably be a subtype of Function.

[johnmyleswhite]

I think we could have a type like this, for when you want to opt-in to characterizing a function by its argument and return types. However it should probably be a subtype of Function.

If you allow name-munging, would you be open to doing something like this at a method-level? I would love to see things like +(a::Float64, b::Float64) be characterized by formal return types. It would make it very easy to produce tools for working with missing data that rival R's very limited supply of built-in types.

[andyferris]

Could we support methods as first-class objects, that we can extract from and add to functions? Functions would just be containers of methods. Each method could have a nominated (or potentially even computed) return type.

[StefanKarpinski]

@andyferris: I rather like the idea of making methods first class. I had a conversation with @JeffBezanson about this some time ago and he had some objections, but I can't recall them. Lots of things would become nicely factorable if Method were a first-class type, e.g. the result of @which f(...) could return a method object; and we could express @code_xxx f(...) as code_xxx(@which f(...)) where the thing passed to code_xxx is a Method object.

[JeffBezanson]

julia> typeof(@which 1+1)
Method

[yuyichao]

The Method doesn't really have all the information needed by code_xxxx though.

[StefanKarpinski]

Right – I would say that at this point Method is semi-first-class (second class?).

[StefanKarpinski]

Things that could make Method more first-class:

• being callable, so e.g. invoke could be expressed as (which(f, types...))(args...)
• allowing a Method object to be added to a Function as @andyferris suggests
• comparison of methods for specificity?

There are probably other things too. I don't think this is a high priority, however.

[yuyichao]

What's non-first class about it? It is the answer to which (i.e. which method) but the answer to that question doesn't contain all the information other code_xxx need since code_typed/llvm/native all need information about specialization (iiuc LambdaInfo)

[JeffBezanson]

I don't think modifying method tables more often is something we want to encourage. But of course, whatever API we have for that is orthogonal to how function types work. If return types are associated with methods, I'm not sure what that implies about the programming model --- do you have to extract methods manually to call certain higher-order functions? We probably don't want that, but the point is we need to work out the syntax and semantics in more detail.

Yes, @which just tells you which definition is called. code_typed is willing to return specializations. I suppose we could have @which return specializations as well, but it didn't seem to make sense to generate a specialization just to find out what definition is called.

Making methods callable is possible, but complicates the system. For example we can optimize map(sin, x) perfectly well. Now we would need to handle map(which(sin, (T,)), x) also. The easiest way to handle this is to have a curried invoke:

invokable(f, types) = (args...)->invoke(f, types, args...)

One way to look at the problem is closures: to call a closure, you need an instance of it that has the expected data fields. You can't call one with just a Method --- unless you're willing to pass a function instance, but at that point you might as well just call the function, or use invoke, or the curried invoke.

[vtjnash]

When #265 is fixed, that would also be the wrong definition for invoke, since method lookup is not separable from inference or call while maintaining a consistent view of the world. (this is another way to state Jeff's comment that there would be a second operation that would need to be optimized, but noting that it this construct may not be actually be inferable).

[aaronsheldon]

Until recently I was of the opinion that functions are objects with types just like everything else, however a theoretical consideration from Mathematical Logic changed my mind.

In their most general form functions can only be defined, or exist, with respect to the Axiom of Choice. This makes functions part of a larger Universe (ZFC) than regular types (ZF). Regular types can be checked through an extrinsic computable algorithm, or certifier. In contrast the general definition of a function is intrinsic and self-referential. Defining a function requires specification of a subset of the Cartesian tuple space (DOM X IMG), such that no element in DOM is represented by more than one tuple in (DOM X IMG). You can only ever define a subset like that, in general, via the Axiom of Choice.

Basically functions are the boundary between where a computer can verify some fact itself (in ZF), and where it has to trust the specification provided by a human (in ZFC). This means that if you wanted to treat functions like fully typed objects you would need to build a full fledged theorem prover for your type inference system that could take an algorithm specified in a function and prove in ZFC that it is a function. (consider the headache of asking the computer to prove sin(x) is a function in Euclidean Geometry before actually being able to call sin(x), i.e. if the ratios of the triangle are fixed then the angle is fixed.)

I apologize for asserting the opposite stance in an earlier issue. I had not thought through the theoretical considerations carefully enough. I also apologize for confounding functions with methods, in this case I mean function in the general mathematical sense.

[StefanKarpinski]

Higher order types of any kind have the same issue but non-well-founded set theories address this issue in a way that embeds ZFC anyway, so this is not nearly as compelling an argument these days as it once was. Julia being a dynamic language, we don't actually care about always being able to check types. Sufficiently expressive static type systems have to give up on this anyway, we just gave up on it from the beginning. What we do care about is tractability of computing the subtype relation.

[aaronsheldon]

hmmm, I'm having trouble with understanding how non-well-founded-ness bypasses the axiom of choice. Perhaps that bit of logical reasoning is intellectually beyond me.

Aside from the obvious constructivists approach I haven't found any references to alternatives to the axiom of choice in the non-well-founded set theory literature (even reaching into Category theory).

But there are plenty of counter examples, e.g. Banach-Tarski, that depend on the axiom of choice, as well as the ability to construct Hamel bases in infinite dimensional Abelian groups, e.g. reals as a vector space over rationals.

[StefanKarpinski]

Functions don't require AC to exist or be defined – you only need the product of two non-empty sets to be non-empty, which is a theorem in ZF. There is a problem with higher kinded types in ZF(C), which is what hypersets address, but it has nothing to do with AC. In languages like Julia where types are themselves objects, one needs at least one type that is a member of itself. Since hypersets can contain themselves, they provide a theoretical basis for this sort of construction. In any case, I don't think any of this is particularly relevant to anything practical wrt Julia.

[tbenst]

@aaronsheldon @StefanKarpinski that may be true for ZF(C) but we can't practically implement this foundation in computer science anyhow. Haskell shows this is possible with a Category Theory foundation, Coq shows it's possible with the Calculus of Constructions, and it's an especially important concept in Homotopy Type Theory.

If I understand @quinnj's idea correctly, it would solve the following issue:

function str_to_int(x :: String)
    return parse(Int,x)
end

function int_to_str(x :: Int)
    return "$(x)"
end

function compose(functions...)
    return reduce((a,f) -> x -> a(f(x)),functions)
end

valid = compose(x -> 2*x,str_to_int,int_to_str)
invalid = compose(x -> 2*x,int_to_str) # should fail type check

valid(2)
invalid(2) # fails here

[martinholters]

If you define *(::Int, ::String) after invalid is defined, invalid(2) works without problems. The order of function/method definition does not matter, as long as everything that is necessary is defined upon calling the function.

[tbenst]

@martinholters fair point, but not what I intended to show. Here's an explicit type annotation, with an arrow used to annotate return type:

function double(x::Int) -> Int
    return x*2

invalid = compose(double,int_to_str) # should fail type check

admittedly this is a contrived example, but the point is that int_to_str::Function{Int,String} and double::Function{Int,Int}, and so under the speculative feature the function composition would throw a type error at compile time.

There are good performance reasons to do this:

1. Safety & modularity: makes it easier to reuse functions in a safe manner, raising errors at compile time at the correct line number
2. Performance: makes it possible to in-line functions in more cases
3. Parallel computing: this type of function composition is very common in map-reduce and is a simple approach to embarrassingly parallel problems. Making composition errors becomes more and more common as pipelines get complex, and it sucks to find out at hours later at run-time instead of at compile-time. Speaking from personal experience in Python/Numpy ;)

[martinholters]

What should happen if I, after I defined your double as above, do

double(x::String) = string(x, x)

? Should that be an error because that method does not match the function signature?

[tbenst]

That's an excellent question. And I think it raises some subtle points. What is the type of a function with multiple dispatch? If functions are values, and not expressions, should they follow lazy or eager evaluation?

I'm not familiar with how multiple dispatch is implemented in Julia, and would welcome links or information so I can learn more. Nevertheless, some speculation follows

Set theory

In this interpretation, we use the union type to represent types with multiple dispatch double::Union{Function{Int,Int}, Function{String,String}}. In order to compile a new function using compose, we have two options:

1. (Eager evaluation) compose always returns a Function or Union{Function}
2. (Lazy evaluation) compose returns Function{Any,Any} unless a type annotation is given

(1) is probably unfeasible as we are unbounded in the number of choices. (Imagine if a function returns a Union type, and the subsequent function has multiple dispatch!). Set theory is great for pure math, but unbounded sets are tough to represent on a computer.

(2) seems much more reasonable

valid = compose(double,str_to_int,int_to_str)::Function{Int, Int}

but this starts to look weird when we consider later defining a new method:

valid = compose(int_to_str,double,str_to_int)::Function{String, String}

Is valid overwritten? Or is it now Union{Function{Int, Int},Function{String, String}}? There seems to be some tension between Methods and Functions.

Category theory

In Haskell, multiple dispatch is implemented through Multi-parameter type class. This approach has proved quite elegant in practice. stack overflow

{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, OverlappingInstances #-}

class (Num a, Num b) => Power a b where
  my_pow :: a -> b -> a

instance Power Double Double where
  my_pow = (**)

instance Num a => Power a Integer where
  my_pow = (^)

Rust opts for a similar implementation using Traits. Rust's type system for Num makes implementing Pow for i32 a bit painful, so just showing the concept with floats instead.

trait Pow {
    fn my_pow(self, other: i32) -> f64;
}

impl Pow for f32 {
    fn my_pow(self, other: i32) -> f64 {self.powi(other) as f64}
}

impl Pow for f64 {
    fn my_pow(self, other: i32) -> f64 {self.powi(other)}
}

Traits seem like a very natural way to think about the value of a Function in Julia. We could use a Trait (abstract type) to represent a particular Function, and each method as a concrete type that implements the Trait.

Homotopy Type theory

Just for fun: under this school of thought, methods could be viewed as homotopy equivalences, and thus each method of a function is actually the same type. But we're probably three years away from a practical first implementation.

[vtjnash]

The Set theory interpretation appears to essentially be Arrow Types? and the observations there about computability (and the breakdown in meaning when presented with multi-methods) are largely why we don't have them.

The category theory examples both seem to demonstrate static dispatch (Julia uses dynamic multiple dispatch, which that SO article mentions isn't possible with the Haskell approach).

[tbenst]

@vtjnash on the same page re: Arrow Types.

I have not seen dynamic multiple dispatch in Haskell but it's unclear to me when this would be useful since the compiler does type inference across the whole program. Seems more likely to be handled by the IO monad followed by static dispatch.

For Rust, it's a different story as type inference is limited to narrower scopes, and the language is less pure. Thus, Rust provides dynamic multiple dispatch via Trait Objects. Given that Julia seems to be headed towards Traits rather than Multiple Inheritance/Type Classes, perhaps this is the better starting point.

[vtjnash]

Homotopy Type theory

This sounds potentially equivalent implementation of Function types in Julia, which essentially asserts that all methods in a function have the same type. However, it's hard to verify if it applies completely. It may also not apply, since Julia simply asserts that all methods are associated with their Function.

I think the most description is to say that they Julia's methods form a partial tiling of the type lattice over the argument tuple (where one of the arguments is the function itself, represented as a first-class value). In such a formulation, you can both assert that you are at a particular node and find the closest matching method. However, it can be a bit cumbersome to need to assert what the input and output types will be, rather than just using the function. In the top example (adjust{A}(f::Function{A,Bool}, ...) = f(A)) it's equivalently expressible as adjust(f) = f(A)::Bool.

[vtjnash]

dynamic multiple dispatch in Haskell

This seems tautological, as the SO article mentions that Haskell's representation is incapable of dynamic multiple dispatch (and that other mechanism are used instead to achieve the same goals; these are all turing-complete languages of course).

Seems more likely to be handled by the IO monad followed by static dispatch.

Yes, but now you have two types of function calls. IIUC, IO monads are a pretty straight-foward implementation of the standard vtable approach to simulating dynamic dispatch in languages that don't implement it natively. Julia just has one type, and makes it fast. They can both be useful, but they have to be respected for their differences in approach.

Thus, Rust provides dynamic multiple dispatch via Trait Objects.

It's dynamic, but it's not multiple dispatch. Like Haskell, it's a vtable-based solution. It might be worthwhile to investigate the difference between that and multiple dispatch: https://en.wikipedia.org/wiki/Virtual_method_table#Comparison_with_alternatives

[tbenst]

This seems tautological, as the SO article mentions that Haskell's representation is incapable of dynamic multiple dispatch (and that other mechanism are used instead to achieve the same goals; these are all turing-complete languages of course).

Haskell's lack of "dynamic" multiple dispatch is because it's a static language. So agreed that there's limits to what we can learn from Haskell towards implementation in Julia, but we can still learn from how Haskell implements multiple dispatch and functions as first-class types via type classes.

It's dynamic, but it's not multiple dispatch. Like Haskell, it's a vtable-based solution.

Right, for multiple dispatch have to use Trait objects with associated types. The RFC that was implemented provides a better overview. The implementation is described in Trait Resolution.

My conjecture is that multiple dynamic dispatch can be thought of as a Trait, and that doing so enables both functions and methods to be first-class types: abstract and concrete, respectively.

[vtjnash]

Discussion moved to https://discourse.julialang.org/t/function-parameter-speculation-17168/1677, since it's speculative about types, and not actually about the top issue.