> 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.
> 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:
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_scienc... )
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
> 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 )
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-...
- Macros https://www.cse.iitk.ac.in/users/ppk/teaching/cs653/notes/le...
- Dependent types 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://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.
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: 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_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
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
> 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.
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 )