Specifying Function Contract

There is lots of good work around specifying the interface of types, their traits, etc. I was curious if I’m missing conversation around declaring the behavior of a function in terms of its arguments somewhat like the signatures of generic functions in static languages.

What I’m thinking about is a syntax something like:

@declare function sum(::T)::E where {T, E = eltype(T)} end

@implement function sum(x)
    reduce(+, x)
end

# expands to:
@generated function sum(x::T) where {T}
    E = eltype(T)
    return :(convert($E, __implemented_sum(x)))
end

function __implemented_sum(x)
    reduce(+, x)
end

Caveats:

  • I’m not married to any specifics on syntax, so I hope you won’t get bogged down on whether the checks should go in where{} or somewhere else.
  • I’m aware that function f()::E end indicates a conversion, but my generated function only uses an assertion. I think the syntax I wrote looks clean, so I’m leaving it as is for now. But I recognize that reconciling the semantic meaning of ::E would be important if this was going to be actually implemented Just switched it to a proper convert so that it respects the function return type annotation semantics.
  • I also don’t know if sum should actually be defined this way. Maybe there are cases where the sum of a series of elements should not result in the same type or a subtype? It’s just something to work off of.

My only point is, should the original owner of a function be able to programmatically specify the relationship between argument types and return types?

A tradeoff of my current approach above is that anyone could define a sum method without @implement and bypass the checks. That’s good for keeping Julia flexible (similar spirit to not having a true private). That’s bad because you could forget to add the macro and miss out on the checks. Leaving it this way would also let you to implement it in Base, theoretically, because it wouldn’t be breaking since regular method definition is left unchanged.

Anyway, I’m curious if this conversation has already happened, and I just missed it!

edit: A bunch of edits to the code to make it more correct

Edit 2: remove hasmethod checks based on discussion below.

3 Likes

GitHub - Keno/InterfaceSpecs.jl: Playground for formal specifications of interfaces in Julia is experimental.

Main Page · RequiredInterfaces.jl is my take on this - the TL;DR is though (as you noticed) that this more or less requires buy-in from Base to be useful, in part because of what to do about dispatch and how these things should interact with it.

2 Likes

This is an interesting take. To me it appears related to the distinction between parametric and ad-hoc polymorphism in Haskell:

  • A generic function is parametric polymorphic if it works with arguments of different types (originally all types, but extended to allow restrictions to certain type classes). Here is an example similar to yours:

    sum :: (Foldable t, Num a) => t a -> a
    sum = foldr (+) 0
    

    The type states precisely the information you want:

    1. The container type[1] t must be Foldable, i.e., implement foldr etc.
    2. The element type a must be Numeric, i.e., implement + etc.

    An important aspect of such a parametric function is that it only has a single implementation which can nevertheless work, e.g., by being instantiated, with different concrete types.

  • A generic function is ad-hoc polymorphic if it’s part of a type-class – which are rather similar to interfaces or traits. In this case, it can have multiple implementations for every concrete type implementing the type class.

    In the above example, foldr is part of the Foldable type-class, and is for instance implemented differently for lists (foldr f z [] = z; foldr f z (x:xs) = f y (foldr f z ys)) or Maybe (foldr f z Nothing = z; foldr f z (Just x) = f x z).

    In this way, a type class specifies which functionality a type must support in order to implement it. From what I understand, Rust uses a similar approach with traits corresponding to the ad-hoc polymorphic part and functions with trait bounds to the parametric polymorphism.

In Julia the situation is considerably more complicated as every function can be written in a generic way, i.e., work for any type adhering to some interface of used methods, as well as being overloaded for different types. In this respect, generic functions could be considered as parametric and ad-hoc polymorphic at the same time. According to this view, your sum example defines a parametric polymorphic function (Imho, the requirement of an iterate method should not be part of it as it’s an implementation detail of reduce – which might or might not actually require it).

Overall, I’m not even sure how to best describe the flexible approach of Julia in a type system at all. Not even considering multiple dispatch which further complicates the situation.


  1. As Haskell has higher-kinded types, the container type t itself can be parametric. Thus, the element type does not need to associated with container, e.g., via eltype, but it’s defined via t a. ↩︎

3 Likes

Thanks, @jar1 and @Sukera! Those are exactly the efforts I was thinking of in my first sentence. I’ll admit, reading the ReadMes for both of those packages makes me realize just how in over my head I am with this stuff.

That said, I think I’m try to do something orthogonal here. I’m not so worried about describing whether a certain type meets the criteria for an interface and testing that rigorously. I’m thinking more in terms of runtime checks where the you can ensure that you get an error when an assumption is violated. Like, if I define iseven(::SomeT)=5, I’d like to get an error that I just called a malformed iseven that returned an Int when it should have returned a Bool. But my thinking on this was hazy when I posted and my original code does obfuscate that goal and made it act a lot more like your interface related work.

Thank you @bertschi for that thoughtful response. You really cut through my muddy post to my point! You’re absolutely right that checking hasmethod isn’t the right approach because someone might implement sum that calls their own functions. All I care about is defining return type in terms of the argument types.

As I’ve been thinking about this more, in a Julia 2.0 where respecting the contract of the function is required, you could use it to solve the Constructor return type problem by just requiring that all implementations of the constructor return the type.

1 Like

The thread Case Study: Method Invalidations caused by Pkg.jl with Julia 1.11 ended up answering a problem here:

Specifically here, given the importance of Symbolics in the Julia ecosystem, the meaning of function names doesn’t always match the mechanical use of those functions. Setting a contract that requires == to return a Bool would be problematic for them.

I am certainly no Core Developer, so I don’t pretend to know the tradeoffs for serving different use cases. But I do wonder if it would be possible to use Cassette.jl to transform all (F)(args...) where F to (F)(SymbolicCall(), args...) that could have its own contract, so that “normal” use cases could benefit from the correctness checks that function contracts could provide.

IMO they shouldn’t have punned == for constructing equations in the first place. == should be a predicate.

4 Likes

I think, regardless of whether one agrees with that specific design choice, the counter example does prove that two thoughtful, experienced developers might want two very different behaviors from the same symbol and that’s part of the beauty of multiple dispatch.

That said, I still come down on the side of giving up some flexibility for the sake of checks and optimizations. I think it is in a similar vein as “sealing” functions.

1 Like

It’s not punned. Your “recommendation” would break all tracing. It doesn’t seem to understand how the tracing works.

1 Like

Do you think there is a way to generally check return types in a similar fashion to what I’m suggesting without doing significant harm to Symbolics?

julia> @variables x y
2-element Vector{Num}:
 x
 y

julia> typeof(x == y)
Num

I’m not sure what are you referring to, but I don’t see how it could be relevant here.

To expand, the way that Symbolics implements == breaks the contract of the == function, which is one of the more important functions.

The approach that Symbolics.jl took may allow it to be useful as a CAS, but prevents it from integrating into the Julia ecosystem well.

2 Likes

One more thought: this idea plus sealing the method table for the declared function would allow users to @implement as many new dispatches as they want but not allow new contracts to be defined.

In the case where the return value is constant, i.e. @declare function iseven(::Any)::Bool, the return type of the function couldn’t be invalidated even though users could make new dispatches.

The contract of == explicitly does not necessarily return a boolean and there is a separate function in Julia if you want to guarantee a boolean, and that’s isequal.

It does this so that it integrates with the Julia ecosystem because it keeps the contracts of the language and uses isequals vs == appropriately. If it did not do this, then it would not work with general functions. This is how come tracing of numerical functions works.

1 Like

The result is of type Bool, except when one of the operands is missing, in which case missing is returned (three-valued logic).

So the return value should be Union{Bool,Missing}.

We should fix that docstring.

I don’t think that making fundamental post-hoc changes to function docstrings is the right approach. I think it would be better to say “The == operator in Symbolics does not follow the generic definition provided in Base Julia, but that is a necessary tradeoff to enable tracing of arbitrary numerical functions.”

When it comes down to it, Julia is a dynamic language, so it’s not possible to guarantee that == returns a boolean. The definition in the Base.== docstring is provided to enable generic programming—it is not provided for type safety or even for compiler optimizations. If a package like Symbolics has a legitimate reason to return a non-Boolean from ==, there is nothing fundamentally wrong with that.

1 Like

I strongly disagree with that. If a programmer can’t trust a docstring, what should they trust in when they want to write code?

Symbolics having a slightly different meaning for == in their DSL is very different from subverting the existing docstring entirely.

3 Likes

I think we are in agreement. What I meant is that there are rare cases where it is reasonable, or at least expedient, to bend the meaning of the docstring, like Symbolics does. And Julia, as a dynamic language, does not prevent that.

I agree that in 99% of cases we want method implementations to follow the generic definition in the docstring.