7 ms·

> Types being correct does not imply values being correct, so you will have to write those tests anyhow, although you maybe be fooled by the safyness of static

> Types being correct does not imply values being correct, so you will have to write those tests anyhow, although you maybe be fooled by the safyness of static typing[1] that you don't have to. Urgh, that reference is such a shallow, straw-man facade of static typing. This is especially evident with its link to https://www.sans.org/top25-software-errors/ https://www.sans.org/top25-software-errors/ and claim that those "don't look like type errors to me", a list which includes: - 16 even says 'type' in the title: "Unrestricted Upload of File with Dangerous Type"! Phrased as a type error, this would be "savePicture: Required argument of type 'Either[PNG, JPEG]', given 'Array[Byte]' instead" - 2, 3, 6, 11, 18 are all injection attacks, which are classic type errors (AKA "stringly typed programming"). Phrased as a type error, these would be "+: Cannot append 'Foo' with 'FormInput'", where 'Foo' might be 'SQL', 'ShellCommand', etc. - NULL pointer dereference is Tony Hoare's 'billion dollar mistake', which as type error would be "Expected 'Foo', given 'null'" - integer over/underflow, buffer over/underflow, out-of-bounds access, etc. can all be mitigated with types like 'Maybe', 'Try', etc. at the cost of a bounds/flag check. If we don't want runtime checks, we can instead track memory usage bounds in the types, and have the compiler check that we're allocating enough. So many of these problems are avoidable with types, even before we go into fancy stuff like dependent types, linear types, etc. In particular, most of the burden to getting this right is on languages and libraries, not application developers. For example, if a database library can only be queried by an 'SQL' type, and the only way to construct that type is via literals and a 'withParam[T]: SQL -> T -> SQL' function, then application developers are unable to introduce injection attacks; the library forces them to do the right thing. Instead we get 'dbQuery: String -> ...', 'runShell: String -> ...', 'response.withBody: String -> ...', etc. and draw the conclusion that types can't help :(

simiones 5y ago
The problem is that often getting rid of these type-unsafe idioms requires much more sophisticated types OR much more tedious code than expected. For example, a language without NULL references must rely on something like Optional/Maybe. Optional requires generic types (kind-1 types) to be usable, and it also requires some kind of pattern matching or monad comprehensions - otherwise, code using Optional is neither type safe nor readable. The SQL case is much more complex. SQL is such a non-standardized language in practice, and such a complex one, that trying to offer a generic SQL library that presents an AST as the API for even the most popular RDBMSs quickly gets complex. So, you end up with convenient string->SQL converters, and then people stick untrusted input in those strings. Not to mention, your fancy AST library still needs to spit out SQL text to talk to most DBs, so you end up needing to sanitize identifiers in your own SQL->string conversion.
- mpweiher 5y ago
  Right. The other thing is that in the parent, "static type checking" got shortened to "types", which in turn got confused with "modelling". The problem with stringly-typing is the model, which is SQL as strings. Statically type-checking that all your strings are, in fact, strings does not buy you anything whatsoever in this scenario. On the other hand, if you have an actual model of the SQL, then it also doesn't matter whether that model is checked at runtime (dynamic typing) or at compile-time (static typing). In either case it will not allow injection attacks, if implemented correctly. And of course the actual place where nastiness happens is the user input, and I haven't yet seen a place that can statically typecheck users. ;-). So, as you point out, you will need to do dynamic checking and sanitising of input.
  - chriswarbo 5y ago
    > And of course the actual place where nastiness happens is the user input, and I haven't yet seen a place that can statically typecheck users. ;-) User input has type `ByteString`. Not only can we check that statically, we absolutely should; and we should enforce that type, to reject any code which assumes otherwise. Nastiness happens when developers treat user input as something other than ByteString; e.g. they might try appending it to a fragment of HTML (XSS); or wrap it in quotation marks and send it to a database (SQL injection). We don't need to 'statically typecheck users'; we do need to statically check that `myApp` has type `ByteString -> Foo`, so we can avoid ever executing implementations which actually have type `HTMLFragment -> Foo` (XSS), or `SQLFragment -> Foo` (SQL injection), or whatever.
  - deleted 5y ago
    [deleted]
  - seanwilson 5y ago
    > On the other hand, if you have an actual model of the SQL, then it also doesn't matter whether that model is checked at runtime (dynamic typing) or at compile-time (static typing). In either case it will not allow injection attacks, if implemented correctly. It's possible to implement anything correctly with dynamic types but the point is static typing makes it easier to do so. Static types will exhaustively check for you that certain errors aren't possible (vs tests that check a finite number of cases) + compile-time (vs at runtime when the error actually occurs on particular inputs). > And of course the actual place where nastiness happens is the user input, and I haven't yet seen a place that can statically typecheck users. ;-). So, as you point out, you will need to do dynamic checking and sanitising of input. It sounds like you're talking about dynamic (type) checking here when you really mean regular runtime behaviour? You absolutely can at compile-time make sure your program is going to respond in a sensible way to problematic user inputs at runtime e.g. the compiler verifies that either the user input string value will get turned into a `valid email` value at runtime or the user is asked to try again. I wouldn't call the condition that checks if the string is a valid email a dynamic type check. I don't see how user input is different or special from any other value either e.g. it's not like you can predict what exact values are going to come from files, random number generators or from complex calculations during runtime, you just care that they're in the range you expect.
mpweiher 5y ago
> "Unrestricted Upload of File with Dangerous Type" You are confusing "type" with "static type". This is user input. You are not going to statically typecheck your users. (See other comment for stringly-typing).
- chriswarbo 5y ago
  > You are confusing "type" with "static type". This is user input. You are not going to statically typecheck your users. You are confusing "type" with "not a function type". Firstly, I absolutely want to check, statically, that my user input is `ByteString`, or `String`, or some more distinguished newtype/AnyVal wrapper around those. If that doesn't pass the type checker, I would be very worried about ever starting such an executable! Other than that, I want to check, statically, that my functions conform to their type signatures. When I write `parsePNG userInput: Maybe PNG`, not only do I want to make damn sure that `userInput: ByteString` is definitely a `ByteString`; I also want to make damn sure that `parsePNG: ByteString -> Maybe PNG` is definitely a (partial) function from `ByteString` to `Maybe PNG`. If I can't guarantee, without executing the program, that `parsePNG` can only return `Maybe PNG` values, then all bets are off regarding downstream invariants, and that's not a good situation to be in w.r.t. security vulnerabilities.
  - mpweiher 5y ago
    > I absolutely want to check, statically, that my user input is `ByteString`, or `String` My condolences, you must have horribly unreliable user widget/user input libraries. My TextFields always deliver a "String" to me (unless I've set them up to deliver numbers). I don't need to check that statically. > You are confusing "type" with "not a function type". No I am not. You don't seem to understand what I meant with "You are not going to statically type check your users".
    - chriswarbo 5y ago
      > My condolences, you must have horribly unreliable user widget/user input libraries The libraries seem pretty reliable; but I'm not (exactly the same as in the SQL example, BTW). For example, I don't think I've ever managed to write a Python3 program which hasn't crashed at some point due to me mixing-up string/bytes; of course, testing doesn't usually find such problems, even with Hypothesis, since I make exactly the same mistakes when I'm writing the tests. I've also written a whole bunch of Python3 programs which spend ages crunching numbers, only to output '<map object at 0x10199c2e0>' instead of printing a list. I make exactly the same mistakes when writing Haskell and Scala; but the computer tells me that I've made a mistake, and how to fix it, before the program ever gets a chance to run. > You don't seem to understand what I meant with "You are not going to statically type check your users". That might be the case. I can't elaborate on what you meant (since I may have misunderstood)
alerighi 5y ago
And there are a ton of other type errors that you cannot catch. For example take a method that wants a string in a particular format, you pass a string in another format and it breaks. A method that wants an integer in a range. An array of maximum N elements. And we can go on forever. So what you do? I find code that uses excessive type checks too verbose, you end up doing things only to make the compiler happy, even if you know that a particular condition will never happen (e.g. a variable that can be null but given a particular condition you know that it cannot be because it was initialized earlier, but the compiler is not smart enough to know). So to me using static types makes sense where types are used by the compiler to produce faster code (embedded contexts, basically, of course I don't use Python on a microcontroller) and as a linting of the code (Python type annotations or Typescript).
- igouy 5y ago
  > For example take a method that wants a string in a particular format, you pass a string in another format and it breaks. "SafeStrings: Representing Strings as Structured Data" https://arxiv.org/abs/1904.11254 https://arxiv.org/abs/1904.11254 Bosque https://github.com/microsoft/BosqueLanguage/blob/master/docs/papers/publist.md#-safestrings-representing-strings-as-structured-data https://github.com/microsoft/BosqueLanguage/blob/master/docs...
- chriswarbo 5y ago
  > For example take a method that wants a string in a particular format, you pass a string in another format and it breaks. This sentence betrays a confusion about what types are, and how to use them. In particular, you seem to be mixing up two possible scenarios. In the first scenario, we have a method which "wants a string" (i.e. its input type is 'String'), and we can "pass a string" (i.e. call it with an argument of type 'String'). This code passes the type-checker, since it implements the specification we gave: accept 'String'. Perhaps there are higher-level concepts like "formats" involved, and the resulting application doesn't work as intended; but that's not the fault of the types. More specifically: typecheckers verify that code implements its specification; but they do not validate that our specification captures the behaviour we want. In the second scenario, we have a method which "wants a string in a particular format" (i.e. its input type is 'Format[A]'), and we "pass a string in another format" (i.e. call it with an argument of type 'Format[B]'). That is a type error, and the typechecker will spot that for us; perhaps pointing us to the exact source of the problem, with a helpful message about what's wrong and possible solutions. We do not get a runnable executable, since there is no meaningful way to interpret the inconsistent statements we have written. tl;dr if you want a typechecker to spot problems, don't tell it that everything's fine! If you want the safety and machine-assistance of such 'Format' types, but also want the convenience of writing them as strings, there are several ways to do it, e.g. - Polymorphism http://okmij.org/ftp/typed-formatting/FPrintScan.html#print-show http://okmij.org/ftp/typed-formatting/FPrintScan.html#print-... - Macros https://www.cse.iitk.ac.in/users/ppk/teaching/cs653/notes/lectures/Template-Haskell-based-printf.lhs.pdf https://www.cse.iitk.ac.in/users/ppk/teaching/cs653/notes/le... - Dependent types https://gist.github.com/chrisdone/672efcd784528b7d0b7e17ad9c115292 https://gist.github.com/chrisdone/672efcd784528b7d0b7e17ad9c... > A method that wants an integer in a range. An array of maximum N elements. And we can go on forever. You're making the same mix-up with all of these. Fundamentatlly: does your method accept a 'Foo' argument (in which case, why complain that it accepts 'Foo' arguments??!) or does it accept a 'FooWithRestriction[R]' argument (in which case, use that type; what's the problem?) Again, there are multiple ways to actually write these sorts of types, depending on preferences and other constraints (e.g. the language we're using). Some examples: - https://hackage.haskell.org/package/fin https://hackage.haskell.org/package/fin - https://ucsd-progsys.github.io/liquidhaskell-blog https://ucsd-progsys.github.io/liquidhaskell-blog Your "integer in a range" is usually called 'Fin n', an array with exactly N elements is usually called 'Vector n t', etc. I don't think there's an "array of maximum N elements" type in any stdlib I've come across, but it would be trivial enough to define, e.g. data ArrayOfAtMost Nat (t: Type) where Nil : {n: Nat} -> ArrayOfAtMost n t Cons : {n: Nat} -> (x: t) -> (a: ArrayOfAtMost n t) -> ArrayOfAtMost (S n) t This is exactly the same as the usual 'Vector' definition (which is a classic "hello world" example for dependent types), except a Nil vector has size zero, whilst a Nil 'ArrayOfAtMost' can have any 'maximum size' we like (specified by its argument 'n'; the {braces} tell the compiler to infer its value from the result type). We use 'Cons' to prepend elements as usual, e.g. to represent an array of maximum size 8, containing 5 elements [a,b,c,d,e] of type 'Foo', we could write: myArray: ArrayOfAtMost 8 Foo myArray = Cons a (Cons b (Cons c (Cons d (Cons e (Nil 3))))) Note that (a) we can write helper functions which make this nicer to write, and (b) just because the code looks like a linked-list, that doesn't actually dictate how we represent it in memory (we could use an array; or we could optimise it away completely https://en.wikipedia.org/wiki/Deforestation_(computer_science) https://en.wikipedia.org/wiki/Deforestation_(computer_scienc... ) I actually wrote a blog post many years ago which goes through various types which have a similar 'Nil and Cons' structure http://chriswarbo.net/blog/2014-12-04-Nat_like_types.html http://chriswarbo.net/blog/2014-12-04-Nat_like_types.html Also note that we don't actually need to write such constraints directly, since we can often read them in from some external specification instead (known as a "type provider"), e.g. a database schema https://studylib.net/doc/18619182 https://studylib.net/doc/18619182 > you end up doing things only to make the compiler happy, even if you know that a particular condition will never happen You might know it, but the compiler doesn't; you can either prove it to the compiler, which is what types are for; or you can just tell the compiler to assume it, via an "escape hatch". For example, in any language which allows non-termination (including Idris, which lets us turn off the termination checker on a case-by-case basis), we can write an infinite loop which has a completely polymorphic type, e.g. -- Haskell version anything: a anything = anything -- Dependent type version anything: (t: Type) -> t anything t = anything t We can use this to write a value of any type the compiler might require. Even Coq, which forbids infinite loops (except for co-induction, which is a whole other topic ;) ) we can tell the compiler to assume anything we like by adding it as an axiom. > So to me using static types makes sense where types are used by the compiler to produce faster code (embedded contexts, basically, of course I don't use Python on a microcontroller) and as a linting of the code (Python type annotations or Typescript). Static types certainly give a compiler more information to work with; although whether the resulting language is faster or not is largely orthogonal (e.g. V8 is a very fast JS interpreter; Typed Racket not so much). As for merely using a type system for linting, that's ignoring most of the benefits. No wonder your code is full of inappropriate types like "string" and "int"! I highly recommend you expand your assumptions about what's possible, and take a look at something like Type Driven Development (e.g. https://www.idris-lang.org https://www.idris-lang.org )

simiones 5y ago

The problem is that often getting rid of these type-unsafe idioms requires much more sophisticated types OR much more tedious code than expected. For example, a language without NULL references must rely on something like Optional/Maybe. Optional requires generic types (kind-1 types) to be usable, and it also requires some kind of pattern matching or monad comprehensions - otherwise, code using Optional is neither type safe nor readable. The SQL case is much more complex. SQL is such a non-standardized language in practice, and such a complex one, that trying to offer a generic SQL library that presents an AST as the API for even the most popular RDBMSs quickly gets complex. So, you end up with convenient string->SQL converters, and then people stick untrusted input in those strings. Not to mention, your fancy AST library still needs to spit out SQL text to talk to most DBs, so you end up needing to sanitize identifiers in your own SQL->string conversion.

mpweiher 5y ago
Right. The other thing is that in the parent, "static type checking" got shortened to "types", which in turn got confused with "modelling". The problem with stringly-typing is the model, which is SQL as strings. Statically type-checking that all your strings are, in fact, strings does not buy you anything whatsoever in this scenario. On the other hand, if you have an actual model of the SQL, then it also doesn't matter whether that model is checked at runtime (dynamic typing) or at compile-time (static typing). In either case it will not allow injection attacks, if implemented correctly. And of course the actual place where nastiness happens is the user input, and I haven't yet seen a place that can statically typecheck users. ;-). So, as you point out, you will need to do dynamic checking and sanitising of input.
- chriswarbo 5y ago
  > And of course the actual place where nastiness happens is the user input, and I haven't yet seen a place that can statically typecheck users. ;-) User input has type `ByteString`. Not only can we check that statically, we absolutely should; and we should enforce that type, to reject any code which assumes otherwise. Nastiness happens when developers treat user input as something other than ByteString; e.g. they might try appending it to a fragment of HTML (XSS); or wrap it in quotation marks and send it to a database (SQL injection). We don't need to 'statically typecheck users'; we do need to statically check that `myApp` has type `ByteString -> Foo`, so we can avoid ever executing implementations which actually have type `HTMLFragment -> Foo` (XSS), or `SQLFragment -> Foo` (SQL injection), or whatever.
- deleted 5y ago
  [deleted]
- seanwilson 5y ago
  > On the other hand, if you have an actual model of the SQL, then it also doesn't matter whether that model is checked at runtime (dynamic typing) or at compile-time (static typing). In either case it will not allow injection attacks, if implemented correctly. It's possible to implement anything correctly with dynamic types but the point is static typing makes it easier to do so. Static types will exhaustively check for you that certain errors aren't possible (vs tests that check a finite number of cases) + compile-time (vs at runtime when the error actually occurs on particular inputs). > And of course the actual place where nastiness happens is the user input, and I haven't yet seen a place that can statically typecheck users. ;-). So, as you point out, you will need to do dynamic checking and sanitising of input. It sounds like you're talking about dynamic (type) checking here when you really mean regular runtime behaviour? You absolutely can at compile-time make sure your program is going to respond in a sensible way to problematic user inputs at runtime e.g. the compiler verifies that either the user input string value will get turned into a `valid email` value at runtime or the user is asked to try again. I wouldn't call the condition that checks if the string is a valid email a dynamic type check. I don't see how user input is different or special from any other value either e.g. it's not like you can predict what exact values are going to come from files, random number generators or from complex calculations during runtime, you just care that they're in the range you expect.

mpweiher 5y ago

> "Unrestricted Upload of File with Dangerous Type" You are confusing "type" with "static type". This is user input. You are not going to statically typecheck your users. (See other comment for stringly-typing).

chriswarbo 5y ago
> You are confusing "type" with "static type". This is user input. You are not going to statically typecheck your users. You are confusing "type" with "not a function type". Firstly, I absolutely want to check, statically, that my user input is `ByteString`, or `String`, or some more distinguished newtype/AnyVal wrapper around those. If that doesn't pass the type checker, I would be very worried about ever starting such an executable! Other than that, I want to check, statically, that my functions conform to their type signatures. When I write `parsePNG userInput: Maybe PNG`, not only do I want to make damn sure that `userInput: ByteString` is definitely a `ByteString`; I also want to make damn sure that `parsePNG: ByteString -> Maybe PNG` is definitely a (partial) function from `ByteString` to `Maybe PNG`. If I can't guarantee, without executing the program, that `parsePNG` can only return `Maybe PNG` values, then all bets are off regarding downstream invariants, and that's not a good situation to be in w.r.t. security vulnerabilities.
- mpweiher 5y ago
  > I absolutely want to check, statically, that my user input is `ByteString`, or `String` My condolences, you must have horribly unreliable user widget/user input libraries. My TextFields always deliver a "String" to me (unless I've set them up to deliver numbers). I don't need to check that statically. > You are confusing "type" with "not a function type". No I am not. You don't seem to understand what I meant with "You are not going to statically type check your users".
  - chriswarbo 5y ago
    > My condolences, you must have horribly unreliable user widget/user input libraries The libraries seem pretty reliable; but I'm not (exactly the same as in the SQL example, BTW). For example, I don't think I've ever managed to write a Python3 program which hasn't crashed at some point due to me mixing-up string/bytes; of course, testing doesn't usually find such problems, even with Hypothesis, since I make exactly the same mistakes when I'm writing the tests. I've also written a whole bunch of Python3 programs which spend ages crunching numbers, only to output '<map object at 0x10199c2e0>' instead of printing a list. I make exactly the same mistakes when writing Haskell and Scala; but the computer tells me that I've made a mistake, and how to fix it, before the program ever gets a chance to run. > You don't seem to understand what I meant with "You are not going to statically type check your users". That might be the case. I can't elaborate on what you meant (since I may have misunderstood)

alerighi 5y ago

And there are a ton of other type errors that you cannot catch. For example take a method that wants a string in a particular format, you pass a string in another format and it breaks. A method that wants an integer in a range. An array of maximum N elements. And we can go on forever. So what you do? I find code that uses excessive type checks too verbose, you end up doing things only to make the compiler happy, even if you know that a particular condition will never happen (e.g. a variable that can be null but given a particular condition you know that it cannot be because it was initialized earlier, but the compiler is not smart enough to know). So to me using static types makes sense where types are used by the compiler to produce faster code (embedded contexts, basically, of course I don't use Python on a microcontroller) and as a linting of the code (Python type annotations or Typescript).

igouy 5y ago
> For example take a method that wants a string in a particular format, you pass a string in another format and it breaks. "SafeStrings: Representing Strings as Structured Data" https://arxiv.org/abs/1904.11254 https://arxiv.org/abs/1904.11254 Bosque https://github.com/microsoft/BosqueLanguage/blob/master/docs/papers/publist.md#-safestrings-representing-strings-as-structured-data https://github.com/microsoft/BosqueLanguage/blob/master/docs...
chriswarbo 5y ago
> For example take a method that wants a string in a particular format, you pass a string in another format and it breaks. This sentence betrays a confusion about what types are, and how to use them. In particular, you seem to be mixing up two possible scenarios. In the first scenario, we have a method which "wants a string" (i.e. its input type is 'String'), and we can "pass a string" (i.e. call it with an argument of type 'String'). This code passes the type-checker, since it implements the specification we gave: accept 'String'. Perhaps there are higher-level concepts like "formats" involved, and the resulting application doesn't work as intended; but that's not the fault of the types. More specifically: typecheckers verify that code implements its specification; but they do not validate that our specification captures the behaviour we want. In the second scenario, we have a method which "wants a string in a particular format" (i.e. its input type is 'Format[A]'), and we "pass a string in another format" (i.e. call it with an argument of type 'Format[B]'). That is a type error, and the typechecker will spot that for us; perhaps pointing us to the exact source of the problem, with a helpful message about what's wrong and possible solutions. We do not get a runnable executable, since there is no meaningful way to interpret the inconsistent statements we have written. tl;dr if you want a typechecker to spot problems, don't tell it that everything's fine! If you want the safety and machine-assistance of such 'Format' types, but also want the convenience of writing them as strings, there are several ways to do it, e.g. - Polymorphism http://okmij.org/ftp/typed-formatting/FPrintScan.html#print-show http://okmij.org/ftp/typed-formatting/FPrintScan.html#print-... - Macros https://www.cse.iitk.ac.in/users/ppk/teaching/cs653/notes/lectures/Template-Haskell-based-printf.lhs.pdf https://www.cse.iitk.ac.in/users/ppk/teaching/cs653/notes/le... - Dependent types https://gist.github.com/chrisdone/672efcd784528b7d0b7e17ad9c115292 https://gist.github.com/chrisdone/672efcd784528b7d0b7e17ad9c... > A method that wants an integer in a range. An array of maximum N elements. And we can go on forever. You're making the same mix-up with all of these. Fundamentatlly: does your method accept a 'Foo' argument (in which case, why complain that it accepts 'Foo' arguments??!) or does it accept a 'FooWithRestriction[R]' argument (in which case, use that type; what's the problem?) Again, there are multiple ways to actually write these sorts of types, depending on preferences and other constraints (e.g. the language we're using). Some examples: - https://hackage.haskell.org/package/fin https://hackage.haskell.org/package/fin - https://ucsd-progsys.github.io/liquidhaskell-blog https://ucsd-progsys.github.io/liquidhaskell-blog Your "integer in a range" is usually called 'Fin n', an array with exactly N elements is usually called 'Vector n t', etc. I don't think there's an "array of maximum N elements" type in any stdlib I've come across, but it would be trivial enough to define, e.g. data ArrayOfAtMost Nat (t: Type) where Nil : {n: Nat} -> ArrayOfAtMost n t Cons : {n: Nat} -> (x: t) -> (a: ArrayOfAtMost n t) -> ArrayOfAtMost (S n) t This is exactly the same as the usual 'Vector' definition (which is a classic "hello world" example for dependent types), except a Nil vector has size zero, whilst a Nil 'ArrayOfAtMost' can have any 'maximum size' we like (specified by its argument 'n'; the {braces} tell the compiler to infer its value from the result type). We use 'Cons' to prepend elements as usual, e.g. to represent an array of maximum size 8, containing 5 elements [a,b,c,d,e] of type 'Foo', we could write: myArray: ArrayOfAtMost 8 Foo myArray = Cons a (Cons b (Cons c (Cons d (Cons e (Nil 3))))) Note that (a) we can write helper functions which make this nicer to write, and (b) just because the code looks like a linked-list, that doesn't actually dictate how we represent it in memory (we could use an array; or we could optimise it away completely https://en.wikipedia.org/wiki/Deforestation_(computer_science) https://en.wikipedia.org/wiki/Deforestation_(computer_scienc... ) I actually wrote a blog post many years ago which goes through various types which have a similar 'Nil and Cons' structure http://chriswarbo.net/blog/2014-12-04-Nat_like_types.html http://chriswarbo.net/blog/2014-12-04-Nat_like_types.html Also note that we don't actually need to write such constraints directly, since we can often read them in from some external specification instead (known as a "type provider"), e.g. a database schema https://studylib.net/doc/18619182 https://studylib.net/doc/18619182 > you end up doing things only to make the compiler happy, even if you know that a particular condition will never happen You might know it, but the compiler doesn't; you can either prove it to the compiler, which is what types are for; or you can just tell the compiler to assume it, via an "escape hatch". For example, in any language which allows non-termination (including Idris, which lets us turn off the termination checker on a case-by-case basis), we can write an infinite loop which has a completely polymorphic type, e.g. -- Haskell version anything: a anything = anything -- Dependent type version anything: (t: Type) -> t anything t = anything t We can use this to write a value of any type the compiler might require. Even Coq, which forbids infinite loops (except for co-induction, which is a whole other topic ;) ) we can tell the compiler to assume anything we like by adding it as an axiom. > So to me using static types makes sense where types are used by the compiler to produce faster code (embedded contexts, basically, of course I don't use Python on a microcontroller) and as a linting of the code (Python type annotations or Typescript). Static types certainly give a compiler more information to work with; although whether the resulting language is faster or not is largely orthogonal (e.g. V8 is a very fast JS interpreter; Typed Racket not so much). As for merely using a type system for linting, that's ignoring most of the benefits. No wonder your code is full of inappropriate types like "string" and "int"! I highly recommend you expand your assumptions about what's possible, and take a look at something like Type Driven Development (e.g. https://www.idris-lang.org https://www.idris-lang.org )