Formal algebra of types

[Jiahao Chen]

- rambling researchy note warning: there is no real point to this post. -

In recent days I have been toying with how to explain the usefulness of a type system for technical computing. Currently I have the notion that data abstraction using types allows a formal separation of the representation of a data type from its interface (functions and methods defined involving that type). So we can define any algebra we want on a type using its interface, and worry later about whether its representation is faithful to the desired algebra.

This led me to wonder about the how much a compiler can "know" about algebra: can a compiler tell if some type T and some operand + form a monoid, or group, or nothing special at all? The main limitation is that static analysis is not allowed to know anything about runtime values of code, so it's hard to test directly properties like commutativity which are universally quantified (in principle you have to test commutativity of every pair of values in the type).

Attached is an IJulia notebook with some experiments I ran. The main tool used is code_typed to infer the output type of operations like T+T. There's also the notion of "formalness"; that in the absence of values the only things you can reason about are input and output types (which I abuse slightly to think about domain and range sets of functions).

 Formal algebra of types.ipynb

​

A couple of thoughts:

- Since type inference is not guaranteed to return a sharp output, the result of testing for algebraic structure using code_typed has to be ternary-valued: yes, no or don't know (insufficient information to decide).

- Some parametric types with non-leaftype parameters, like Rational{Union(Uint, Int)} and Complex{Integer}, turn out _not_ to be type-closed under + because of internal promotion rules in the arithmetic. Other parametric types like Vector{Int} don't touch promotion rules and are hence type-closed. To me, this was quite a non-obvious interaction of type promotion and parametric invariance.

- The compiler doesn't know whether or not (Matrix{Float64}, *) forms a group because one(::Matrix{Float64}) cannot be defined - without size information, there is not enough data to compute the multiplicative identity.  The compiler also doesn't know whether or not (Union(UniformScaling{Float64}, Matrix{Float64}, *) has an inverse, but arguably we can define a method for one() that returns I for one::(Union(UniformScaling, anything_else...)) that is correct.

Thoughts and suggestions welcomed.

Jiahao Chen

Staff Research Scientist
MIT Computer Science and Artificial Intelligence Laboratory

[Stefan Karpinski]

Could you post this on nbviewer?

[Jiahao Chen]

I couldn't figure out how to get Google Drive and nbviewer to work together, so here is a gist copy:

http://nbviewer.ipython.org/gist/jiahao/b0d4279cec83b681d95f

[Mauro]

Thanks Jiahao, that was an interesting read. Could your `istypeclosed`
function not use `Base.return_types(f, Ts)` instead of parsing
`code_typed`?

And now a bit of self-promotion: I recently thought about uses of
Base.return_types when implementing traits/interfaces in
https://github.com/mauro3/Traits.jl . After reading this I got round to
implement using return types as well. So now with Traits.jl you can
define a trait for a (mathematical) group:

```
julia> using Traits

julia> @traitdef Group{X,Y} begin # a trait defining a group
@constraints begin
X==Y
end
*(X,Y) -> X
*(X,Y,X) -> X
one(X) -> X
inv(X) -> X
end

julia> istrait(Group{Int,Int}, verbose=true)
Method `inv` with signature ((Int64,),(Int64,)) has wrong return type: (Float64,)
false

julia> istrait(Group{Array{Float64,2}, Array{Float64,2}}, verbose=true) # should be true though!
Method `inv` with signature ((Array{Float64,2},),(Array{Float64,2},)) has wrong return type: (Any,)
false

julia> istrait(Group{Float64, Float64})
true

julia> @traitfn f{X; Group{X,X}}(x::X, y::X) = inv(x*y*y)
f (generic function with 4 methods)

julia> f(5,6)
ERROR: TraitException("No matching trait found for function f")
in traitdispatch at /home/mauro/.julia/v0.4/Traits/src/traitfns.jl:252
in f at /home/mauro/.julia/v0.4/Traits/src/traitfns.jl:333

julia> f(5.,6.)
0.005555555555555556
```

Mauro

[Jiahao Chen]

Thanks,

Jiahao Chen
Staff Research Scientist
MIT Computer Science and Artificial Intelligence Laboratory

On Tue, Oct 28, 2014 at 9:11 AM, Mauro <maur...@runbox.com> wrote:

Thanks Jiahao, that was an interesting read.  Could your `istypeclosed`
function not use `Base.return_types(f, Ts)` instead of parsing
`code_typed`?

Yes but I happened to need code_typed to read in the input types to each specific method anyway, and I needed to have the input and output types associated to each method.

And now a bit of self-promotion: I recently thought about uses of
Base.return_types when implementing traits/interfaces in
https://github.com/mauro3/Traits.jl . After reading this I got round to
implement using return types as well.  So now with Traits.jl you can
define a trait for a (mathematical) group:

I like it!

julia> istrait(Group{Array{Float64,2}, Array{Float64,2}}, verbose=true) # should be true though!
Method `inv` with signature ((Array{Float64,2},),(Array{Float64,2},)) has wrong return type: (Any,)
false

The issue here is that "false" means both "not type-closed" and "can't tell if type-closed", because Any is a strict supertype of the input type Matrix{Float64} and type inference in Julia is not guaranteed to be sharp (i.e. Any is not the tightest possible description of the output type, merely an upper bound). This is Case 2 in my notebook, which really should have truth-value "unknown due to insufficient information".

[Mauro]

>> Thanks Jiahao, that was an interesting read. Could your `istypeclosed`
>> function not use `Base.return_types(f, Ts)` instead of parsing
>> `code_typed`?
>>
> Yes but I happened to need code_typed to read in the input types to each
> specific method anyway, and I needed to have the input and output types
> associated to each method.

I'll need to have a closer look at that. I suspect that this or
something similar is what Traits.jl should do as well. Both signature &
return type checking are a bit too simple at the moment.