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

**URL:** <https://discourse.julialang.org/t/what-are-julias-coordinates-in-the-cube/89883>\
**Category:** Internals & Design\
**Tags:** question, type\
**Created:** [November 7, 2022, 2:25pm UTC](https://discourse.julialang.org/t/what-are-julias-coordinates-in-the-cube/89883 "2022-11-07T14:25:13Z")\
**Posts on this page:** 7\
**Page:** 1

<div class="post-metadata">

**Author:** ![cdawg](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/cdawg/32/9811_2.png) [@cdawg](https://discourse.julialang.org/u/cdawg)\
**Post date:** [November 7, 2022, 2:25pm UTC](https://discourse.julialang.org/t/what-are-julias-coordinates-in-the-cube/89883/1 "2022-11-07T14:25:13Z")

</div>

I was sidetracked procrastinating reading a thread about using “{}”. [here](https://discourse.julialang.org/t/why-begin-end-instead-of-for-block-delimiter/89735/2) 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

```julia
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:

> **[Lambda cube](https://en.wikipedia.org/wiki/Lambda_cube)**
>
> In mathematical logic and type theory, the λ-cube (also written lambda cube) is a framework introduced by Henk Barendregt to investigate the different dimensions in which the calculus of constructions is a generalization of the simply typed λ-calculus. Each dimension of the cube corresponds to a new kind of dependency between terms and types. Here, "dependency" refers to the capacity of a term or type to bind a term or type. The respective dimensions of the λ-cube correspond to:
> The different wa...

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.

---

<div class="post-metadata">

**Author:** ![Sukera](https://avatars.discourse-cdn.com/v4/letter/s/ce7236/32.png) [@Sukera](https://discourse.julialang.org/u/Sukera)\
**Post date:** [November 7, 2022, 2:38pm UTC](https://discourse.julialang.org/t/what-are-julias-coordinates-in-the-cube/89883/2 "2022-11-07T14:38:53Z")

</div>

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

```julia
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” 🙂

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… 🙂

---

<div class="post-metadata">

**Author:** ![DNF](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/dnf/32/10191_2.png) [@DNF](https://discourse.julialang.org/u/DNF)\
**Post date:** [November 7, 2022, 2:49pm UTC](https://discourse.julialang.org/t/what-are-julias-coordinates-in-the-cube/89883/3 "2022-11-07T14:49:57Z")

</div>

This is the one thing I would love to see:

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

```

Does that also fall into the pit of compiler havoc?

---

<div class="post-metadata">

**Author:** ![cdawg](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/cdawg/32/9811_2.png) [@cdawg](https://discourse.julialang.org/u/cdawg)\
**Post date:** [November 7, 2022, 3:29pm UTC](https://discourse.julialang.org/t/what-are-julias-coordinates-in-the-cube/89883/4 "2022-11-07T15:29:12Z")

</div>

` Val{X+Y}()` 🤯

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!!!**

---

<div class="post-metadata">

**Author:** ![Sukera](https://avatars.discourse-cdn.com/v4/letter/s/ce7236/32.png) [@Sukera](https://discourse.julialang.org/u/Sukera)\
**Post date:** [November 7, 2022, 3:49pm UTC](https://discourse.julialang.org/t/what-are-julias-coordinates-in-the-cube/89883/5 "2022-11-07T15:49:39Z")

</div>

> [@DNF](#):
>
> Does that also fall into the pit of compiler havoc?

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`:

```julia
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.

---

<div class="post-metadata">

**Author:** ![anon56330260](https://avatars.discourse-cdn.com/v4/letter/a/f07891/32.png) [@anon56330260](https://discourse.julialang.org/u/anon56330260)\
**Post date:** [November 7, 2022, 4:33pm UTC](https://discourse.julialang.org/t/what-are-julias-coordinates-in-the-cube/89883/6 "2022-11-07T16:33:21Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![oxinabox](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/oxinabox/32/206603_2.png) [@oxinabox](https://discourse.julialang.org/u/oxinabox)\
**Post date:** [November 7, 2022, 4:51pm UTC](https://discourse.julialang.org/t/what-are-julias-coordinates-in-the-cube/89883/7 "2022-11-07T16:51:51Z")

</div>

> [@cdawg](#):
>
> Actually, doesn’t Julia already, on some level, have dependent types?

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.