Yes, this is much more accurate. However you’ve left out an entire, rather important class of functions: constructors. Fixing that is not too hard however, we just need to account for the type of the called object also. It’s also can be a bit confusing to call them Function, since it is a somewhat ambiguous and overloaded term. I prefer to refer to this is the set of all methods in the system.
julia> f(x::Number) = x
Tuple{typeof(f), Number} --> Number
julia> f(x::String) = x
Tuple{typeof(f), String} --> String
julia> f{T<:Union{Number, String}}(x::T, n::Number) --> T = x^n
(Tuple{typeof(f), T, Number} --> T) where T <: Union{Number, String}
julia> methods()
Union{every signature in the system}
and would be improved by traits
Not really. Notice that with the formulation used by Julia (translated into your syntax) used for that last one can already be optimally computed and represented in the type system.
type checker would verify proper subtyping
No, this doesn’t actually logically follow. I mean, it sort of does, but it’s best to avoid skipping a mention of the intermediate step where you’ve just provided a solution to the halting problem 
But still good food for thought. It would be nice to have a way to express that signature <: A implies return <: B. Or for a concrete example, to express that convert(::Type{T}, ::Any)::T, aka that (Tuple{typeof(convert), Type{T}, Any} --> T) where T <: Any.