What are Julia's coordinates in the λ-cube?

Internals & Design
,
1

I was sidetracked procrastinating reading a thread about using “{}”. here and popping out a new thread.

My vote was to make where statements more expressive by doing type calculations inside blocks deliminated by {} so you could do obvious things like

function outer(SMatrix{N,M,T}, SMatrix{O,P,T})::SMatrix{Q,R,T} 
where {T, Q = N*O, R = M*P}
...
end

and @Sukera mentioned that this causes compiler havoc. And I can see why. Fully dependent types are clearly a bad idea. Things can be circular, types depending on values which must be determined after running which causes compilation. This is somewhat hinted at in the article on the Lambda cube:

where it’s implied λC is a little crazy. But I wasn’t thinking about fully dependent types. Looking at the lambda cube, Julia is quite close to Fω, it has dispatch
(types → values )
and constructors
(types → types)
But these constructors are highly limited, all you can really do is make an S expression out of them, delimited by {}, and manipulate these S-expressions via where statements and constructors. I was really thinking about making (types → types) more expressive, where the functions can only capture other type parameters, not values.

@Sukera is still right. If {} could use multiplication, it would depend on Base.* and everything in global to do calculations, and then we have the full madness of dependent types.

Q1: But still why are the Julia functions (types → types) so limited? Actually, I don’t really know how limited it is. Can we define arithmetic on types? Isn’t this already what is done in some sense but only for typeinfer? Can we extend the arithmetic on types? Can somebody build a Lisp out of only curly braces in Julia today? If the answer is no, would it be a bad thing if we could?

Q2: Actually, doesn’t Julia already, on some level, have dependent types? After all, when we use Val, somehow a value ends up in curly brackets, halo and harp and all. Are these dangerous exceptions brought about by necessity, or hints that the language could be much more expressive or both?

Q3: Since everything is callable, what even distinguishes a type from a value…and now my brain hurts and I understand nothing.

Just interested in design choice and necessity, and thinking. I’m very happy with Julia although I find types difficult, and don’t understand why they are so hard to manipulate.

2 Likes
2

Great questions! I don’t have time to have a full discussion right now, but let me add this as food for thought:

julia> foo(::Val{X}, ::Val{Y}) where {X,Y} = Val{X+Y}()
foo (generic function with 1 method)

julia> @code_warntype foo(Val(1), Val(2))
MethodInstance for foo(::Val{1}, ::Val{2})
  from foo(::Val{X}, ::Val{Y}) where {X, Y} @ Main REPL[1]:1
Static Parameters
  X = 1
  Y = 2
Arguments
  #self#::Core.Const(foo)
  _::Core.Const(Val{1}())
  _::Core.Const(Val{2}())
Body::Val{3}
1 ─ %1 = ($(Expr(:static_parameter, 1)) + $(Expr(:static_parameter, 2)))::Core.Const(3)
│   %2 = Core.apply_type(Main.Val, %1)::Core.Const(Val{3})
│   %3 = (%2)()::Core.Const(Val{3}())
└──      return %3

It’s fully typestable, even though we’re doing “computation” on a “value” that came from a type, and constructing a new type based on that result! What I mean to say is that there is A LOT of stuff you can do with statically known, isbits type parameters. We can do a lot of (constant foldable) computation with type parameters, which is not limited to Int. The trouble is that we can’t do method selection based on pattern matching or some other boolean function (i.e. a function foo(x, y)::Bool) in dispatch and adding that (especially with user defined foo) is what’s difficult and almost instantly spirals down into a discussion about traits, multiple abstract supertypes and similar (well trodden, not so easily summarized) topics.

It’s good to remember though that the lambda cube and similar classifications (like type theory as a whole) came after the languages that they describe, so there may not be a simple answer like “julia is in corner X of the cube” :slight_smile:

In any case, I encourage you to play around with exactly how much is possible with isbits type parameters - you might be surprised to find much more than just peano being possible… :slight_smile:

2 Likes
3

This is the one thing I would love to see:

struct MyStruct{T, N}
    S::SVector{T, N+1}
end

Does that also fall into the pit of compiler havoc?

4

Val{X+Y}() :exploding_head:

Obviously, I absolutely did not know you could do math {inside type parameters}!!! And even if you could, I would never expect it to be type stable!!!

5

As written, yes. You can enforce it in the constructor, if you add another type parameter to MyStruct or make the type of S part of the type parameter of MyStruct:

struct MyStruct{T, N, M}
    S::SVector{T, M}
    MyStruct{T,N}(...) where {T,N} = MyStruct{T, N, N+1}(...)
end

But if you just want to have N, you’re going to lose the semantic guarantee that the second type parameter of S is N+1 or risk making field access type unstable (since the type of the field is then no longer determined by the type of MyStruct alone).

Since computation with type parameters in functions is perfectly fine though, you can easily just do N-1 in your callsites and it will probably, if the type it sees in inference is not a UnionAll with an unknown in N, constant fold the calculation.

6

According to wikipedia’s description, you need to have function types to discuss the lambda cube, see the Product and Abstraction rules. Therefore, this concept is totally meaningless for Julia (and any other dynamic languages) or Julia has only a trivial type system (where every thing is typed as any). So Julia is not even at the bottom of lambda cube (STLC). In contrast, C/C++ is at least STLC if you don’t treat template as part of the type system …

Note : The top of lambda cube is CoC, a type system also used by Coq proofer, which indeed allows all kinds of type calculation. But such languages cannot have specializations like multiple dispatch in Julia, though you can stimulate one by adding constraints, which is expressed through predicates. For example, suppose you only want to define arithmetic operations on some kinds of number types but not other arbitrary types, let’s say abs which returns the absolute value of a number. You declare a constraint called Num a. Num a will be true if type a is number type, like UInt16/UInt8, then the function abs will have the type abs : Num a => a -> a -> a, when you call abs, you need to insert a proof of Num a so you can call abs. So it’s a rather elaborate process.

In Coq, sometimes you need to convert equivalent types by writing proofs to pass type checking, because type checking is undecidable (you can’t judge whether A = B because types can contain terms). This is also how people embed proof in the system by expressing propositions as types.

2 Likes
7

By dictionary definition julia has dependent types.
By what almost anyone from the PL theory community really means when they say dependent types, julia does not have dependent types.

1 Like