Comment by lacker

You can do that in python using https://github.com/patrick-kidger/torchtyping

looks like this:

    def batch_outer_product(x:   TensorType["batch", "x_channels"],
                            y:   TensorType["batch", "y_channels"]
                            ) -> TensorType["batch", "x_channels", "y_channels"]:

    return x.unsqueeze(-1) * y.unsqueeze(-2)

There's also https://github.com/thomasahle/tensorgrad which uses sympy for "axis" dimension variables:

    b, x, y = sp.symbols("b x y")
    X = tg.Variable("X", b, x)
    Y = tg.Variable("Y", b, y)
    W = tg.Variable("W", x, y)
    XWmY = X @ W - Y

> In general, neither can ensure at compile time that an index only known at runtime is in bounds, even if the bounds themselves are statically known.

Yeah, this seems like matrixes might not be a great first example for explaining the value of dependent types. It's fully possible to define a matrix that uses a generic type as the index for each dimension that doesn't allow expressing values outside the expected range; it would just be fairly cumbersome, and the usual issues would creep back in if you needed to go from "normal" integers back to indexes (although not if you only needed to convert the indexes to normal integers).

I find that the potential utility of dependent types is more clear when thinking about types where the "dimensions" are mutable, which isn't usually how I'd expect most people to use matrixes. Even a simple example like "the current length of a list can be part of the type, so you define a method to get the first element only on non-empty lists rather than needing them to return an optional value". While you could sort of implement this in a similar as described above with a custom integer-like type, the limitations of this kind of approach for a theoretically unbounded length are a lot more apparent than a matrix with constant-sized dimensions.

Yes, the point of dependent types is that they give you the ability to do some sort of almost arbitrary (though not strictly Turing-complete) "computation" as part of type checking, which essentially dispenses with the phase separation between "compiling" and "running" code - or at least makes compile-time computation unusually powerful. So if you want to replicate the properties of dependent typing in these existing languages you'll need to leverage their existing facilities for compile-time metaprogramming.

> A proper dependently-typed language can prevent runtime out-of-bound errors even if neither the indices nor the bounds are known at type check time.

Yes, but the way this is done is by threading a proof "this index is within bounds" throughout the code. At runtime (e.g. within 'extracted' code, if you're using common dependently-typed systems), this simply amounts to relying on a kind of capability or ghost 'token' that attests to the validity of that code. You "manufacture" the capability as part of an explicit runtime check when needed (e.g. if the "index" or "bounds" come from user input) and simply rely on it as part of the code.

The latter is what would be most useful imo. Even Matlab can type check matrix sizes with constants these days, but I often wish I could use variables to express relationships between the sizes of different dimensions of inputs to a function.

That's a good point, for example in Eigen you can do

Eigen::Matrix<float, 10, 5>

I just really want it in Python because that's where I do most of my matrix manipulation nowadays. I guess you also would really like it to handle non-constants. It would be nice if these complicated library functions like

torch.nn.MultiheadAttention(embed_dim, num_heads, dropout=0.0, bias=True, add_bias_kv=False, add_zero_attn=False, kdim=None, vdim=None, batch_first=False, device=None, dtype=None)

would actually typecheck that kdim and vdim are correct, and ensure that I correctly pass a K x V matrix and not a V x K one.

In Common Lisp:

  (defparameter *test-array*
    (make-array '(10 5)
                :element-type 'Float
                :initial-element 0.0))

  (typep *test-array* '(Array Float (10 5)))

And the type check will return true.

C has such types and can guarantee that there is no out-of-bounds access at run-time in the scenarios you describe: https://godbolt.org/z/f7Tz7EvfE This is one reason why I think that C - despite all the naysayers - is actually perfectly positioned to address bounds-safe programming.

Often in dependently-types languages one also tries to prove at compile-time that the dynamic index is inside the dynamic bound at run-time, but this depends.

"In general, neither can ensure at compile time that an index only known at runtime is in bounds, even if the bounds themselves are statically known."

I remember being able to use telescopes [1] in Haskell long time ago, around 2012 or so.

[1] https://www.pls-lab.org/en/telescope

Haskell was not and is not properly dependently typed.

Yeah, I just meant proposition-as-types. Sloppy terminology by me. I meant to complain about the general conflation of the "proving system" and the "typechecking system".

Generally in dependent type systems you are limited in some way in what sort of values a type can refer to. The fancy type checking happens at compile time, and then at run time some or most of the type information is erased. The implementation is tricky but the more difficult problem IMO is the developer experience; it involves a lot of extra work to express dependent types and help the compiler verify them.

Type checking is done statically without running the program. You don't need to execute any run-time logic to perform a check like this. What you are suggesting is a much, much weaker form of verification that doesn't require any type system at all.

Can these constraints be statically checked with mypy or a language server?