5 ms·

The issue that I have with Python type hints is they they don't go nearly far enough in describing the data being manipulated. Specifically, I'm thinking of stu

The issue that I have with Python type hints is they they don't go nearly far enough in describing the data being manipulated. Specifically, I'm thinking of stuff like the dimensionality and cardinality of Numpy arrays or Pandas frames. Usually that's the stuff where I have most questions when I look at Python code and the type system as it's being used now offers no help there.

Jeff_Brown 4y ago
You want dependent types!
- Spivak 4y ago
  Python can actually do (some) dependent types with generics but it's not pretty. The only real use-case that is both possible and worthwhile I've found is being able to say a value is a T if there's a default and an Optional[T] otherwise.
  - still_grokking 4y ago
    > Python can actually do (some) dependent types with generics Could you show some examples?
OJFord 4y ago
I'm not sure how a python annotation/type system could possibly do that? If numpy/pandas had different types for different cardinalities it would work today. You just need those libraries to embrace it really, then you could theoretically have type constructors that provide well-typed NxM matrix types or whatever, allowing you to enforce that [[1,2],[3,4]] is an instance of matrix_t(2, 2). I don't see how python could possibly make such inferences for arbitrary libraries.
- Mehdi2277 4y ago
  PEP 646 Variadic generics, https://peps.python.org/pep-0646/ https://peps.python.org/pep-0646/, was made for this specific use case but mypy is still working on implementing it. And even with it, it's expected several more peps are needed to make operations on variadic types powerful enough to handle common array operations. numpy/tensorflow/etc do broadcasting a lot and that probably would need a type level operator Broadcast just to encode that. I also expect the type definitions for numpy will go fairly complex similar to template heavy C++ code after they add shape types.
ramraj07 4y ago
Create a class what enforces this and use the new class as a type?
- abraxas 4y ago
  The trouble is that's not how any of the ML or data science Python code is written at the moment. Such practices could help although I think more elegant solutions should be explored.
hansvm 4y ago
I like typing that with strings like '(batch,r,a,s,channel,t)'. The tooling doesn't do anything special with it, but it makes the code understandable at a glance. Adopting libraries like einops and core routines like einsum in lieu of equivalent alternatives encourages the propagation of names (rather than rolling axes or whatever) anywhere it matters. Having a coding convention about the standard order of axes helps a bit as people get more familiar with that aspect of the codebase too, only deviating where necessary.
- ghotli 4y ago
  I like this comment because so far I don't know what you're talking about. That's the hallmark of something in this domain worth looking up but I figured you might be willing to share more on the matter. :)
  - hansvm 4y ago
    The premise is that Python's type hints don't provide enough information about things like numpy arrays. Fixing that correctly is hard because things that matter in that sort of code include facts which could hypothetically be encoded in a type system: 1. What's the datatype of the array elements 2. Does this array alias other memory 3. Is the access pattern I want to do contiguous in memory 4. If you track the provenance of an array, does it include something like a "width" dimension and a "height" dimension 5. How many dimensions are there 6. What's a good semantic description (type) for each dimension 7. As an exact integer (or modulo some power of 2 or whatever), how big is each dimension And on and on and on. An honest-to-goodness type hint capturing that sort of crap in a way that's statically analyzable is a nightmare, and it wouldn't be totally trivial to even write the code to make a type hint like that reasonable to read and write. Even if you could, it'd probably generate a lot of noise that for any particular use of an array would distract you from the aspects you care about. A nice hybrid solution IMO is found in that Python allows arbitrary objects to be used as type hints, and a string description of the aspects you're using/providing on a particular array works as decent documentation for other developers. For a few examples: 1. The array should describe a typical 24-bit 3-channel image. You might use a type hint like 'u8:(w,h,3)' to indicate that it's a 0-255 integer field rather than a 0-1 float field, which dimensions have width/height/channels, and that it's a 3-channel image. It'd probably be good to also label those channels with a convention like 'u8:(w,h,(rgb))', like 'u8:(w,h,3):rgb', with hungarian typing, or something (no particular recommendations on my end since I'm not usually working with heterogeneous data like that, but choosing the wrong encoding or even the wrong coordinate space for RGB or whatever is a big deal, so you'd probably want to represent that somehow). 2. You have a function signature with multiple inputs, and the computation is mostly arbitrary, but it's important some dimensions align. Then label them the same. Something like matmul(left: '(n, d)', right: '(d, k)') -> '(n, k)'. 3. You're doing some ML thing on some time-series medical data, and it's common t' have giant dense tensors floating around. Label semantically what all the dimensions are with a type like `(batch, r, a, s, channel, t)', or using longer names as appropriate depending on your audience and the background knowledge you can assume. Libraries like einops and functions like `np.einsum` take that a step further and require stringified descriptions of the operation you're trying to do. They can have a learning curve, but the crux of the idea is that instead of writing garbage like `arr[3,6,-4:,np.newaxis,...].T.reshape(4 n, -1)` or God-forbid some sort of roll/transpose logic, you have a higher-level description. A couple examples with einsum: 1. The dot product of v and w is `np.dot(v, w)` or `np.sum(v w) # imagine there's an asterisk; HN's parser is smarter than me`, and it's also `np.einsum('d,d', v, w)`. Arguably einsum is a bit of syntactic noise for such a simple example, but if v and w have different shapes than you think then the simpler solutions will silently produce garbage (e.g., the first option will do matrix multiplications sometimes, and the second is arguably closer to correct most of the time, but if you think you're operating on 1D objects and actually do want a channeled operation like matrix multiplication when the input isn't 1D then the sum of products is wrong and not captured in the type system), but einsum will just barf if the stated dimensions don't match your expectations. Moreover, with optimize=True it'll actually fall back to whichever of the simpler solutions is fastest. 2. Imagine you have a matrix A of shape (n, n) and a matrix X of shape (n, d) and want to compute something like A @ v @ A.T for each column v of X. You can write it via standard numpy operators, but it looks like garbage and kind of hides what's actually happening. The einsum solution is just `np.einsum('vw,wd,nv->nd', A, X, A)`. You're contracting over `v` and `w` and left with `n` and `d`. It's not perfect since you just get single-letter names to work with, but it's a hell of a lot better than equivalent options, and much easier to make suitably fast (just pass optimize=True). And then einops is even better because roll/transpose logic is incredibly fiddly and prone to off-by-one errors in your choice of dimension or needing to deeply understand how the function works to not make footgun-style mistakes. An API like `swapaxes(arr, 'batch', 'time')` is 10x easier to use than `swapaxes(arr, 0, 5)` -- like, imagine somebody adding an extra dimension in a world where positions are absolutely referenced and where if you get it wrong the program will still run and produce interesting-looking garbage because the definitions of `np.dot` and everything else in the library depend on the shape of the inputs.
Epa095 4y ago
You very quickly get undecidable type checking with such a powerful typesystem. Then you need a way to handle that, usually the solution is to help the type checker along by providing a proof that your code inhabits the claimed type. Then you need a way to have the proof live together with the code, a proof language, and preferably a whole library of proofs people can build on. If this sounds fun then you can go play with e.g idris or F*.
- gdprrrr 4y ago
  C++, Java and Rust seem to do well with undecidable type checking.

Jeff_Brown 4y ago

You want dependent types!

Spivak 4y ago
Python can actually do (some) dependent types with generics but it's not pretty. The only real use-case that is both possible and worthwhile I've found is being able to say a value is a T if there's a default and an Optional[T] otherwise.
- still_grokking 4y ago
  > Python can actually do (some) dependent types with generics Could you show some examples?

OJFord 4y ago

I'm not sure how a python annotation/type system could possibly do that? If numpy/pandas had different types for different cardinalities it would work today. You just need those libraries to embrace it really, then you could theoretically have type constructors that provide well-typed NxM matrix types or whatever, allowing you to enforce that [[1,2],[3,4]] is an instance of matrix_t(2, 2). I don't see how python could possibly make such inferences for arbitrary libraries.

Mehdi2277 4y ago
PEP 646 Variadic generics, https://peps.python.org/pep-0646/ https://peps.python.org/pep-0646/, was made for this specific use case but mypy is still working on implementing it. And even with it, it's expected several more peps are needed to make operations on variadic types powerful enough to handle common array operations. numpy/tensorflow/etc do broadcasting a lot and that probably would need a type level operator Broadcast just to encode that. I also expect the type definitions for numpy will go fairly complex similar to template heavy C++ code after they add shape types.

ramraj07 4y ago

Create a class what enforces this and use the new class as a type?

abraxas 4y ago
The trouble is that's not how any of the ML or data science Python code is written at the moment. Such practices could help although I think more elegant solutions should be explored.

hansvm 4y ago

I like typing that with strings like '(batch,r,a,s,channel,t)'. The tooling doesn't do anything special with it, but it makes the code understandable at a glance. Adopting libraries like einops and core routines like einsum in lieu of equivalent alternatives encourages the propagation of names (rather than rolling axes or whatever) anywhere it matters. Having a coding convention about the standard order of axes helps a bit as people get more familiar with that aspect of the codebase too, only deviating where necessary.

ghotli 4y ago
I like this comment because so far I don't know what you're talking about. That's the hallmark of something in this domain worth looking up but I figured you might be willing to share more on the matter. :)
- hansvm 4y ago
  The premise is that Python's type hints don't provide enough information about things like numpy arrays. Fixing that correctly is hard because things that matter in that sort of code include facts which could hypothetically be encoded in a type system: 1. What's the datatype of the array elements 2. Does this array alias other memory 3. Is the access pattern I want to do contiguous in memory 4. If you track the provenance of an array, does it include something like a "width" dimension and a "height" dimension 5. How many dimensions are there 6. What's a good semantic description (type) for each dimension 7. As an exact integer (or modulo some power of 2 or whatever), how big is each dimension And on and on and on. An honest-to-goodness type hint capturing that sort of crap in a way that's statically analyzable is a nightmare, and it wouldn't be totally trivial to even write the code to make a type hint like that reasonable to read and write. Even if you could, it'd probably generate a lot of noise that for any particular use of an array would distract you from the aspects you care about. A nice hybrid solution IMO is found in that Python allows arbitrary objects to be used as type hints, and a string description of the aspects you're using/providing on a particular array works as decent documentation for other developers. For a few examples: 1. The array should describe a typical 24-bit 3-channel image. You might use a type hint like 'u8:(w,h,3)' to indicate that it's a 0-255 integer field rather than a 0-1 float field, which dimensions have width/height/channels, and that it's a 3-channel image. It'd probably be good to also label those channels with a convention like 'u8:(w,h,(rgb))', like 'u8:(w,h,3):rgb', with hungarian typing, or something (no particular recommendations on my end since I'm not usually working with heterogeneous data like that, but choosing the wrong encoding or even the wrong coordinate space for RGB or whatever is a big deal, so you'd probably want to represent that somehow). 2. You have a function signature with multiple inputs, and the computation is mostly arbitrary, but it's important some dimensions align. Then label them the same. Something like matmul(left: '(n, d)', right: '(d, k)') -> '(n, k)'. 3. You're doing some ML thing on some time-series medical data, and it's common t' have giant dense tensors floating around. Label semantically what all the dimensions are with a type like `(batch, r, a, s, channel, t)', or using longer names as appropriate depending on your audience and the background knowledge you can assume. Libraries like einops and functions like `np.einsum` take that a step further and require stringified descriptions of the operation you're trying to do. They can have a learning curve, but the crux of the idea is that instead of writing garbage like `arr[3,6,-4:,np.newaxis,...].T.reshape(4 n, -1)` or God-forbid some sort of roll/transpose logic, you have a higher-level description. A couple examples with einsum: 1. The dot product of v and w is `np.dot(v, w)` or `np.sum(v w) # imagine there's an asterisk; HN's parser is smarter than me`, and it's also `np.einsum('d,d', v, w)`. Arguably einsum is a bit of syntactic noise for such a simple example, but if v and w have different shapes than you think then the simpler solutions will silently produce garbage (e.g., the first option will do matrix multiplications sometimes, and the second is arguably closer to correct most of the time, but if you think you're operating on 1D objects and actually do want a channeled operation like matrix multiplication when the input isn't 1D then the sum of products is wrong and not captured in the type system), but einsum will just barf if the stated dimensions don't match your expectations. Moreover, with optimize=True it'll actually fall back to whichever of the simpler solutions is fastest. 2. Imagine you have a matrix A of shape (n, n) and a matrix X of shape (n, d) and want to compute something like A @ v @ A.T for each column v of X. You can write it via standard numpy operators, but it looks like garbage and kind of hides what's actually happening. The einsum solution is just `np.einsum('vw,wd,nv->nd', A, X, A)`. You're contracting over `v` and `w` and left with `n` and `d`. It's not perfect since you just get single-letter names to work with, but it's a hell of a lot better than equivalent options, and much easier to make suitably fast (just pass optimize=True). And then einops is even better because roll/transpose logic is incredibly fiddly and prone to off-by-one errors in your choice of dimension or needing to deeply understand how the function works to not make footgun-style mistakes. An API like `swapaxes(arr, 'batch', 'time')` is 10x easier to use than `swapaxes(arr, 0, 5)` -- like, imagine somebody adding an extra dimension in a world where positions are absolutely referenced and where if you get it wrong the program will still run and produce interesting-looking garbage because the definitions of `np.dot` and everything else in the library depend on the shape of the inputs.

Epa095 4y ago

You very quickly get undecidable type checking with such a powerful typesystem. Then you need a way to handle that, usually the solution is to help the type checker along by providing a proof that your code inhabits the claimed type. Then you need a way to have the proof live together with the code, a proof language, and preferably a whole library of proofs people can build on. If this sounds fun then you can go play with e.g idris or F*.

gdprrrr 4y ago
C++, Java and Rust seem to do well with undecidable type checking.