3 ms·

The dependence on library authors is always a challenge in any language. You might have one author using `[a]` where another uses `PositiveNumeric a, Fin n => N

The dependence on library authors is always a challenge in any language. You might have one author using `[a]` where another uses `PositiveNumeric a, Fin n => NonEmptyList n a` for the same thing. You can always just annotate whatever the library author used (e.g. they return a list of strings, so you use List[str]). There are some interesting further add ons that seem very python, allowing you to go further. For example, with a pandas dataframe you can just say your type is a dataframe which isn't so useful, but it's possible to hack your own types onto it in the vein of https://github.com/CedricFR/dataenforce https://github.com/CedricFR/dataenforce, or use things like https://smarie.github.io/python-vtypes/ https://smarie.github.io/python-vtypes/ to get smarter typing on things the authors didn't type. I expect that trend will continue. What fascinates me about python's types is actually the very fact that they are bolted on. You have a language that lets you do crazy things and a type system trying to catch up and make it convenient to verify those crazy things. It's a nice complement to the usual developments of verifying all of the things and slowly extending the set of things you can do.

lmm 6y ago
> You might have one author using `[a]` where another uses `PositiveNumeric a, Fin n => NonEmptyList n a` for the same thing. You can always just annotate whatever the library author used (e.g. they return a list of strings, so you use List[str]). The difference between these two cases is that a function that returns [a] will always return [a] and if you convert it to `NonEmptyList n a` you will be nudged towards handling the case where it didn't actually return n elements, whereas if you annotate someone else's list as returning List[str] then it may well silently not do some of the time, and you won't get an error until a long way away.
- 6gvONxR4sf7o 6y ago
  I was unclear. I meant the other way around. In the case that the third party code does in fact always return no empty lists of positive numbers, the author might just type it as a list. A third party author in even a language like Haskell won’t necessarily use the bells and whistles of giving very specific types. And by the List[str] bit, I mean you can annotate it as doing whatever it in fact does. You aren’t protected if you get that wrong, of course, and that’s where things like stubs come in to help.
  - lmm 6y ago
    > In the case that the third party code does in fact always return no empty lists of positive numbers, the author might just type it as a list. Yes - but as I said, you can be confident that the list type is accurate, and if you want to convert that list to a specific-length list type then you're nudged towards doing it in a way where you handle the case where the list isn't actually the length you specified. > And by the List[str] bit, I mean you can annotate it as doing whatever it in fact does. You aren’t protected if you get that wrong, of course Not "of course"; the whole point of a type system is that it's automatically checked and therefore you can have reasonable confidence in the types you're given.
    - 6gvONxR4sf7o 6y ago
      > You aren’t protected if you get that wrong, of course, and that’s where things like stubs come in to help.
      - lmm 6y ago
        They don't really though? Stubs are just as unchecked as writing the type signature yourself, so even if they're correct at a given point in time, they'll tend to become incorrect for subsequent releases of the libraries they cover.

lmm 6y ago

> You might have one author using `[a]` where another uses `PositiveNumeric a, Fin n => NonEmptyList n a` for the same thing. You can always just annotate whatever the library author used (e.g. they return a list of strings, so you use List[str]). The difference between these two cases is that a function that returns [a] will always return [a] and if you convert it to `NonEmptyList n a` you will be nudged towards handling the case where it didn't actually return n elements, whereas if you annotate someone else's list as returning List[str] then it may well silently not do some of the time, and you won't get an error until a long way away.

6gvONxR4sf7o 6y ago
I was unclear. I meant the other way around. In the case that the third party code does in fact always return no empty lists of positive numbers, the author might just type it as a list. A third party author in even a language like Haskell won’t necessarily use the bells and whistles of giving very specific types. And by the List[str] bit, I mean you can annotate it as doing whatever it in fact does. You aren’t protected if you get that wrong, of course, and that’s where things like stubs come in to help.
- lmm 6y ago
  > In the case that the third party code does in fact always return no empty lists of positive numbers, the author might just type it as a list. Yes - but as I said, you can be confident that the list type is accurate, and if you want to convert that list to a specific-length list type then you're nudged towards doing it in a way where you handle the case where the list isn't actually the length you specified. > And by the List[str] bit, I mean you can annotate it as doing whatever it in fact does. You aren’t protected if you get that wrong, of course Not "of course"; the whole point of a type system is that it's automatically checked and therefore you can have reasonable confidence in the types you're given.
  - 6gvONxR4sf7o 6y ago
    > You aren’t protected if you get that wrong, of course, and that’s where things like stubs come in to help.
    - lmm 6y ago
      They don't really though? Stubs are just as unchecked as writing the type signature yourself, so even if they're correct at a given point in time, they'll tend to become incorrect for subsequent releases of the libraries they cover.