# Specifying Function Contract
**URL:** https://discourse.julialang.org/t/specifying-function-contract/108983
**Category:** Internals & Design
**Created:** [January 18, 2024, 8:24pm UTC](https://discourse.julialang.org/t/specifying-function-contract/108983 "2024-01-18T20:24:57Z")
**Posts on this page:** 18
**Page:** 1
### Author:  [@mrufsvold](https://discourse.julialang.org/u/mrufsvold)
#### Post date: [January 18, 2024, 8:24pm UTC](https://discourse.julialang.org/t/specifying-function-contract/108983/1 "2024-01-18T20:24:58Z")
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:
```julia
@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.
---
### Author:  [@jar1](https://discourse.julialang.org/u/jar1)
#### Post date: [January 19, 2024, 1:32am UTC](https://discourse.julialang.org/t/specifying-function-contract/108983/2 "2024-01-19T01:32:17Z")
[GitHub - Keno/InterfaceSpecs.jl: Playground for formal specifications of interfaces in Julia](https://github.com/Keno/InterfaceSpecs.jl) is experimental.
---
### Author:  [@Sukera](https://discourse.julialang.org/u/Sukera)
#### Post date: [January 19, 2024, 1:38am UTC](https://discourse.julialang.org/t/specifying-function-contract/108983/3 "2024-01-19T01:38:39Z")
[Main Page · RequiredInterfaces.jl](https://seelengrab.github.io/RequiredInterfaces.jl/stable/) 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.
---
### Author:  [@bertschi](https://discourse.julialang.org/u/bertschi)
#### Post date: [January 19, 2024, 8:40pm UTC](https://discourse.julialang.org/t/specifying-function-contract/108983/4 "2024-01-19T20:40:03Z")
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:
- 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 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`.
---
### Author:  [@mrufsvold](https://discourse.julialang.org/u/mrufsvold)
#### Post date: [January 20, 2024, 3:02am UTC](https://discourse.julialang.org/t/specifying-function-contract/108983/5 "2024-01-20T03:02:35Z")
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.
---
### Author:  [@mrufsvold](https://discourse.julialang.org/u/mrufsvold)
#### Post date: [January 22, 2024, 5:23pm UTC](https://discourse.julialang.org/t/specifying-function-contract/108983/6 "2024-01-22T17:23:11Z")
The thread [Case Study: Method Invalidations caused by Pkg.jl with Julia 1.11](https://discourse.julialang.org/t/case-study-method-invalidations-caused-by-pkg-jl-with-julia-1-11/109038/11) ended up answering a problem here:
> [@Case Study: Method Invalidations caused by Pkg.jl with Julia 1.11](https://discourse.julialang.org/t/case-study-method-invalidations-caused-by-pkg-jl-with-julia-1-11/109038/11):
>
> I think a nice example of that `(::Any == ::Any)::Bool` which is perfectly fine in Base as the only return type from `==` in Base, but then any symbolic representation of code turns `==` into something symbolic and every code with a type-unstable `==` recompiles due to Symbolics existing. The problem is, if `==` “should” only ever return a Boolean (which I don’t think should be the case, there’s other counter examples), then we should get an error for violating the rule.
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.
---
### Author:  [@nsajko](https://discourse.julialang.org/u/nsajko)
#### Post date: [January 22, 2024, 5:25pm UTC](https://discourse.julialang.org/t/specifying-function-contract/108983/7 "2024-01-22T17:25:26Z")
> [@mrufsvold](#):
>
> 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.
IMO they shouldn’t have punned `==` for constructing equations in the first place. `==` should be a predicate.
---
### Author:  [@mrufsvold](https://discourse.julialang.org/u/mrufsvold)
#### Post date: [January 22, 2024, 8:06pm UTC](https://discourse.julialang.org/t/specifying-function-contract/108983/8 "2024-01-22T20:06:12Z")
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.
---
### Author:  [@ChrisRackauckas](https://discourse.julialang.org/u/ChrisRackauckas)
#### Post date: [January 23, 2024, 12:03am UTC](https://discourse.julialang.org/t/specifying-function-contract/108983/9 "2024-01-23T00:03:56Z")
> [@nsajko](#):
>
> IMO they shouldn’t have punned `==` for constructing equations in the first place. `==` should be a predicate
It’s not punned. Your “recommendation” would break all tracing. It doesn’t seem to understand how the tracing works.
---
### Author:  [@mrufsvold](https://discourse.julialang.org/u/mrufsvold)
#### Post date: [January 23, 2024, 12:20am UTC](https://discourse.julialang.org/t/specifying-function-contract/108983/10 "2024-01-23T00:20:42Z")
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?
---
### Author:  [@nsajko](https://discourse.julialang.org/u/nsajko)
#### Post date: [January 23, 2024, 1:05am UTC](https://discourse.julialang.org/t/specifying-function-contract/108983/11 "2024-01-23T01:05:52Z")
> [@ChrisRackauckas](#):
>
> It’s not punned.
```julia-repl
julia> @variables x y
2-element Vector{Num}:
x
y
julia> typeof(x == y)
Num
```
> [@ChrisRackauckas](#):
>
> Your “recommendation” would break all tracing. It doesn’t seem to understand how the tracing works.
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](https://docs.julialang.org/en/v1/base/math/#Base.:==) 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.
---
### Author:  [@mrufsvold](https://discourse.julialang.org/u/mrufsvold)
#### Post date: [January 23, 2024, 1:54am UTC](https://discourse.julialang.org/t/specifying-function-contract/108983/12 "2024-01-23T01:54:09Z")
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.
---
### Author:  [@ChrisRackauckas](https://discourse.julialang.org/u/ChrisRackauckas)
#### Post date: [January 23, 2024, 6:44am UTC](https://discourse.julialang.org/t/specifying-function-contract/108983/13 "2024-01-23T06:44:01Z")
> [@nsajko](#):
>
> To expand, the way that Symbolics implements `==` breaks the [contract](https://docs.julialang.org/en/v1/base/math/#Base.:==) of the `==` function, which is one of the more important functions.
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`.
> [@nsajko](#):
>
> The approach that [Symbolics.jl](https://juliahub.com/ui/Packages/Symbolics) took may allow it to be useful as a CAS, but prevents it from integrating into the Julia ecosystem well.
It does this so that it integrates with the Julia ecosystem because it keeps the contracts of the language and uses `isequal`s 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.
---
### Author:  [@nsajko](https://discourse.julialang.org/u/nsajko)
#### Post date: [January 23, 2024, 6:49am UTC](https://discourse.julialang.org/t/specifying-function-contract/108983/14 "2024-01-23T06:49:51Z")
> [@ChrisRackauckas](#):
>
> 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`.
> 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}`.
---
### Author:  [@ChrisRackauckas](https://discourse.julialang.org/u/ChrisRackauckas)
#### Post date: [January 23, 2024, 7:21am UTC](https://discourse.julialang.org/t/specifying-function-contract/108983/15 "2024-01-23T07:21:39Z")
We should fix that docstring.
---
### Author:  [@CameronBieganek](https://discourse.julialang.org/u/CameronBieganek)
#### Post date: [January 23, 2024, 4:41pm UTC](https://discourse.julialang.org/t/specifying-function-contract/108983/16 "2024-01-23T16:41:40Z")
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.
---
### Author:  [@Sukera](https://discourse.julialang.org/u/Sukera)
#### Post date: [January 23, 2024, 5:05pm UTC](https://discourse.julialang.org/t/specifying-function-contract/108983/17 "2024-01-23T17:05:12Z")
> [@CameronBieganek](#):
>
> 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.
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.
---
### Author:  [@CameronBieganek](https://discourse.julialang.org/u/CameronBieganek)
#### Post date: [January 23, 2024, 5:22pm UTC](https://discourse.julialang.org/t/specifying-function-contract/108983/18 "2024-01-23T17:22:10Z")
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.