6 ms·

> 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

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

etbebl 1y 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.
zozbot234 1y 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 1y 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 1y 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.
    - wk_end 1y ago
      It's not that simple, right? Because the computation can actually rely on the types, so the types can't always just be erased. The complexity around knowing when the types are going to be erased or not is part of what motivated Idris 2's adoption of quantities. https://idris2.readthedocs.io/en/latest/updates/updates.html#new-core-language-quantities-in-types https://idris2.readthedocs.io/en/latest/updates/updates.html...
      - codebje 1y ago
        QTT is about clarity on erasing values rather than types, eg, if you define 'Vect n a' do you need to set aside space in the memory structure for a vector for 'n' or not. The types themselves are not represented. If, eg, you wanted to implement something that printed out its own type, like: vname : Vect n a -> String vname = "Vect " ++ show n ++ " " ++ nameOf a Then (1) you'd be requiring "n" to be represented at run-time (so a QTT value of "unrestricted"), and (2) you'd need a type class to find "nameOf" for "a" when executing, because the actual type of "a" is gone. At runtime a type class means a table of methods passed to the function so it can call the right "nameOf" implementation. class Named a where nameOf a : String vname : Named a => Vect n a -> String ≡ vname : String -> Vect n a -> String
lacker 1y 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 1y ago
  Python is a dynamic language where everything happens at run time, including checks of variable types. So you can already do this.
  - nephanth 1y 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")
    - eru 1y ago
      I think Python actually has multiple, different static typechecking systems, depending on which checker you use. Python itself only gives you type annotations, but doesn't specify what they are supposed to mean. (I think. Please correct me if I am wrong.)
      - nephanth 1y ago
        You are slightly wrong. Python does allow you to put anything in annotations. ( pep 3107 that defines type annotations says that explicitly [1]). But it also defines a type checking annotations, which is a specific convention for using pep 3107 annotations. Type annotations were introduced in PEP 484 and updated in a lot of subsequent peps. The python typing system is fully specified in [3]. It does have several implementations, although the reference implementation is mypy [1]: https://peps.python.org/pep-3107/#rejected-proposals https://peps.python.org/pep-3107/#rejected-proposals [2]: https://peps.python.org/pep-0484/ https://peps.python.org/pep-0484/ [3]: https://typing.python.org/en/latest/spec/index.html https://typing.python.org/en/latest/spec/index.html
thomasahle 1y ago
You can do that in python using https://github.com/patrick-kidger/torchtyping 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 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
- patrickkidger 1y ago
  Quick heads-up that these days I recommend https://github.com/patrick-kidger/jaxtyping https://github.com/patrick-kidger/jaxtyping over the older repository you've linked there. I learnt a lot the first time around, so the newer one is much better :)
  - thomasahle 1y ago
    Ah, I would have never thought jaxtyping supports torch :)
- ydj 1y 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 1y 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)
uecker 1y 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 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.
- turndown 1y 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 1y ago
    This is in ISO C99. In C11 it was made an optional feature but in C23 we made the type part mandatory again.
- Sharlin 1y 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 1y 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.
deleted 1y ago
[deleted]
saghm 1y 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 1y 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).
  - eru 1y ago
    You don't need dependent types for that, either.
    - codebje 1y ago
      Not for matrix multiplication, because there's no term-level chicanery to worry about; you just need phantom types for the two dimensions on your matrix type. You can express a lot just carrying phantom types around and using basic pattern matching: in Rust I can express multiplication, concatenation of vectors to matrices, and inverses of square matrices, using phantom types. But I can't say this, or anything remotely like it: struct Matrix<M: u32, N: u32, T> { dim: (M, N), // imaginary dependently typed vectors cells: Vec<M, Vec<N, T>>, } impl<M, N, T> Matrix<M, N, T> { fn mul<O: u32>(&self, &other: Matrix<N, O, T>) -> Matrix<M, O, T> { let cells: Vec<self.m, Vec<other.o, T>> = do_the_thing(); Matrix { // any other values in dim, or a different type in cells, would be a type error dim: (self.m, other.o), cells } } } In other words, there's no dependent pair construction without dependent types. (Or at least dependent kinds and some tricks.)
tmtvl 1y 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 1y ago
  Compile-time checks is what's implied in virtually all these conversations. Does that check run at compile time?
  - tmtvl 1y 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)).
    - chongli 1y ago
      Can you replace 10 5 and 3 3 with variable names and still get the warning without first calling the function?
      - tmtvl 1y ago
        No. You can replace them with asterisks to mean 'any length is fine', but you can't at compile time check something that's only known at runtime (granted, you could see that it can't match if the variables are, for example, an (Integer 1 10) and an (Integer 75 100)). Something you can do with variables is: (defvar *example-dimension* 20) (deftype Example-Array (element-type minor-dimension) `(Array ,element-type (,*example-dimension* ,minor-dimension))) ...and then you can declare variables to be something like, say, (Example-Array Boolean 5) and have it expand to (Array Boolean (20 5)). But the type declaration needs to be of the form (Array &optional element-type dimensions) where dimensions can be any of the following: - An asterisk, which means anything goes. - A number, which means the array needs to have that many dimensions (so an (Array Fixnum 2) is a 2-dimensional array of fixnums). - A list of numbers, asterisks, or a combination of the two, where an asterisk means 'this dimension can be anything' and the numbers mean exactly what you would expect. Maybe something like that would be possible with Coalton, but I haven't played around a lot with that yet.
thesz 1y 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 https://www.pls-lab.org/en/telescope Haskell was not and is not properly dependently typed.

etbebl 1y 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.

zozbot234 1y 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 1y 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 1y 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.
  - wk_end 1y ago
    It's not that simple, right? Because the computation can actually rely on the types, so the types can't always just be erased. The complexity around knowing when the types are going to be erased or not is part of what motivated Idris 2's adoption of quantities. https://idris2.readthedocs.io/en/latest/updates/updates.html#new-core-language-quantities-in-types https://idris2.readthedocs.io/en/latest/updates/updates.html...
    - codebje 1y ago
      QTT is about clarity on erasing values rather than types, eg, if you define 'Vect n a' do you need to set aside space in the memory structure for a vector for 'n' or not. The types themselves are not represented. If, eg, you wanted to implement something that printed out its own type, like: vname : Vect n a -> String vname = "Vect " ++ show n ++ " " ++ nameOf a Then (1) you'd be requiring "n" to be represented at run-time (so a QTT value of "unrestricted"), and (2) you'd need a type class to find "nameOf" for "a" when executing, because the actual type of "a" is gone. At runtime a type class means a table of methods passed to the function so it can call the right "nameOf" implementation. class Named a where nameOf a : String vname : Named a => Vect n a -> String ≡ vname : String -> Vect n a -> String

lacker 1y 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 1y ago
Python is a dynamic language where everything happens at run time, including checks of variable types. So you can already do this.
- nephanth 1y 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")
  - eru 1y ago
    I think Python actually has multiple, different static typechecking systems, depending on which checker you use. Python itself only gives you type annotations, but doesn't specify what they are supposed to mean. (I think. Please correct me if I am wrong.)
    - nephanth 1y ago
      You are slightly wrong. Python does allow you to put anything in annotations. ( pep 3107 that defines type annotations says that explicitly [1]). But it also defines a type checking annotations, which is a specific convention for using pep 3107 annotations. Type annotations were introduced in PEP 484 and updated in a lot of subsequent peps. The python typing system is fully specified in [3]. It does have several implementations, although the reference implementation is mypy [1]: https://peps.python.org/pep-3107/#rejected-proposals https://peps.python.org/pep-3107/#rejected-proposals [2]: https://peps.python.org/pep-0484/ https://peps.python.org/pep-0484/ [3]: https://typing.python.org/en/latest/spec/index.html https://typing.python.org/en/latest/spec/index.html

thomasahle 1y ago

You can do that in python using https://github.com/patrick-kidger/torchtyping 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 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

patrickkidger 1y ago
Quick heads-up that these days I recommend https://github.com/patrick-kidger/jaxtyping https://github.com/patrick-kidger/jaxtyping over the older repository you've linked there. I learnt a lot the first time around, so the newer one is much better :)
- thomasahle 1y ago
  Ah, I would have never thought jaxtyping supports torch :)
ydj 1y 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 1y 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)

uecker 1y 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 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.

turndown 1y 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 1y ago
  This is in ISO C99. In C11 it was made an optional feature but in C23 we made the type part mandatory again.
Sharlin 1y 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 1y 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.

deleted 1y ago

[deleted]

saghm 1y 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 1y 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).
- eru 1y ago
  You don't need dependent types for that, either.
  - codebje 1y ago
    Not for matrix multiplication, because there's no term-level chicanery to worry about; you just need phantom types for the two dimensions on your matrix type. You can express a lot just carrying phantom types around and using basic pattern matching: in Rust I can express multiplication, concatenation of vectors to matrices, and inverses of square matrices, using phantom types. But I can't say this, or anything remotely like it: struct Matrix<M: u32, N: u32, T> { dim: (M, N), // imaginary dependently typed vectors cells: Vec<M, Vec<N, T>>, } impl<M, N, T> Matrix<M, N, T> { fn mul<O: u32>(&self, &other: Matrix<N, O, T>) -> Matrix<M, O, T> { let cells: Vec<self.m, Vec<other.o, T>> = do_the_thing(); Matrix { // any other values in dim, or a different type in cells, would be a type error dim: (self.m, other.o), cells } } } In other words, there's no dependent pair construction without dependent types. (Or at least dependent kinds and some tricks.)

tmtvl 1y 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 1y ago
Compile-time checks is what's implied in virtually all these conversations. Does that check run at compile time?
- tmtvl 1y 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)).
  - chongli 1y ago
    Can you replace 10 5 and 3 3 with variable names and still get the warning without first calling the function?
    - tmtvl 1y ago
      No. You can replace them with asterisks to mean 'any length is fine', but you can't at compile time check something that's only known at runtime (granted, you could see that it can't match if the variables are, for example, an (Integer 1 10) and an (Integer 75 100)). Something you can do with variables is: (defvar *example-dimension* 20) (deftype Example-Array (element-type minor-dimension) `(Array ,element-type (,*example-dimension* ,minor-dimension))) ...and then you can declare variables to be something like, say, (Example-Array Boolean 5) and have it expand to (Array Boolean (20 5)). But the type declaration needs to be of the form (Array &optional element-type dimensions) where dimensions can be any of the following: - An asterisk, which means anything goes. - A number, which means the array needs to have that many dimensions (so an (Array Fixnum 2) is a 2-dimensional array of fixnums). - A list of numbers, asterisks, or a combination of the two, where an asterisk means 'this dimension can be anything' and the numbers mean exactly what you would expect. Maybe something like that would be possible with Coalton, but I haven't played around a lot with that yet.

thesz 1y 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 https://www.pls-lab.org/en/telescope Haskell was not and is not properly dependently typed.