← Back to context

Comment by Sharlin

9 days ago

> For example, I wish Python had the ability to express "a 10 x 5 matrix of float32s" as a type

To clarify, as long as 5 and 10 are constants, this is entirely possible in C++ and Rust^1, neither of which are dependently typed (or at most are dependently typed in a very weak sense). 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. 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.

^1 And weakly in many other languages whose builtin array types have compile-time bounds. But C++ and Rust let user-defined generic types abstract over constant values.

47 comments

Sharlin

Reply
thomasahle  9 days ago

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

  • ydj  8 days ago

    Is there a mypy plugin or other tool to check this via static analysis before runtime? To my knowledge jaxtyping can only be checked at runtime.

    • thomasahle  8 days ago

      I doubt it, since jaxtyping supports some quite advanced stuff:

          def full(size: int, fill: float) -> Float[Array, "{size}"]:
        return jax.numpy.full((size,), fill)

    class SomeClass:
        some_value = 5

        def full(self, fill: float) -> Float[Array, "{self.some_value}+3"]:
            return jax.numpy.full((self.some_value + 3,), fill)

saghm  9 days ago

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

  • jyounker  8 days ago

    The advantage of dependent typing systems is that you can say that the arguments to a matrix multiplication function must have dimensions (m, i) and (i, n) and that result will have dimensions (m, n).

    • akst  8 days ago

      As others have said, this isn't a unique value proposition of dependent types, by all means dependent types provide a solution to this, but so do many other approaches.

      You can do this in C++ & Rust, and I've done something similar in Typescript. The point of the comment you're replying to is kind of making the point that pitches for dependent types probably should give examples of something not already solved by other systems (not that you can't do this in DT). See:

      > Yeah, this seems like matrixes might not be a great first example for explaining the value of dependent types.

      In order to adopt DT, you need to pay a combined cost of productivity loss in terms of established tooling and choose to forgo any human capital which is no longer applicable once you start using a language with Dependent types, and a loss of time spent learning to use a language that has dependent types, which almost certainly has a smaller library ecosystem than most mainstream languages without DT.

      For that reason it's worth considering what examples illustrate a benefit that outweighs all the above costs. I don't think it's enough to simply assert some moral basis on safety when clearly salaries for work done in unsafe languages are already considerably high.

      4 replies →

zozbot234  9 days ago

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.

  • gpderetta  8 days ago

    You can do arbitrary computations as part of type checking in C++, yet I don't think it should be considered dependently typed.

    It seems to me that dependent typing strictly requires going from runtime values to types.

    (You can parametrize types by runtime values in c++ in a trivial sense, by enumerating a finite set a compile time and then picking the correct type at runtime according to a runtime value, still I don't think it counts as the set of valid types would be finite).

    • zozbot234  8 days ago

      The "runtime" values of a dependent type system are not quite runtime values either, because the computation is happening at compile time. When you "extract" a program from a dependently-typed to an ordinary programming language that can compile down to a binary, the dependent types are simply erased and replaced with ordinary, non-dependent types; though there may be "magic" casts in the resulting program that can only be proven correct via dependent types.

      7 replies →

etbebl  9 days ago

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.

lacker  9 days ago

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.

  • zozbot234  9 days ago

    Python is a dynamic language where everything happens at run time, including checks of variable types. So you can already do this.

    • nephanth  9 days ago

      Python has static typechecking which, while not perfect, works pretty well as long as you're not actually trying to circumvent it (or manipulating things "too dynamically")

      2 replies →

    • bluGill  9 days ago

      The problem with runtime is when you make a mistake it can be a long time before you find out. Compile time means a large class of problems is prevented without perfect test coverage. On a small project it isn't a big deal but when you have hundgeds of developers over decades you will miss something

tmtvl  9 days ago

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.

  • ndr  8 days ago

    Compile-time checks is what's implied in virtually all these conversations.

    Does that check run at compile time?

    • tmtvl  8 days ago

      If I define a function foo which takes an (Array Float (10 5)) and then define a function bar which uses the result of calling foo with an (Array String (3 3)) then SBCL will print a warning. If I don't redefine foo and call bar with such an array then a condition will be raised. It's not quite the same as, say Rust's 'thing just won't compile', but that's due to the interactive nature of Common Lisp (I believe someone called it the difference between a living language and a dead language (though the conventional meaning of living language and dead language in programming is a bit different)).

      3 replies →

uecker  9 days ago

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.

  • Sharlin  9 days ago

    -fsanitize-bounds uses a runtime address sanitizer, surely? The program compiles fine. In a (strongly) dependently typed language, something like the following would refuse to typecheck:

      int foo(int i) {
      int bar[4] = { 1, 2, 3, 4 };
      return bar[i]
  }

    The type checker would demand a proof that i is in bounds, for example

      int foo(int i) {
      int bar[4] = { 1, 2, 3, 4 };
      if i < 4
          return bar[i]
      else 
          return 0
  }

    In languages with an Option type this could of course be written without dependent types in a way that's still correct by construction, for example Rust:

      fn foo(i: 32) -> i32 {
      let bar = [1, 2, 3, 4];
      bar.get(i)       // returns Option<i32>, not a raw i32
         .unwrap_or(0) // provide a default, now we always have an i32
  }

    But ultimately, memory safety here is only guaranteed by the library, not by the type system.

    • uecker  9 days ago

      You seem to be repeating what I said except you mixup strong and static typing. In a statically dependent-typed language you might expect it this not to compile, but this also depends. Run-time checking is certainly something you can combine with strong dependent typing.

      Implementing bounds checking that returns option types (which can also implement in C) is not exactly the same thing. But dependent typing can be more elegant - as it is here.

      1 reply →

  • turndown  9 days ago

    I thought that this was a GCC extension(you need to use #define n 10 instead of int n = 10). Is this not the case anymore?

    • uecker  9 days ago

      This is in ISO C99. In C11 it was made an optional feature but in C23 we made the type part mandatory again.

thesz  8 days ago

"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.