I read the argument in the article as something like “strong advanced type systems like Haskell’s are good because instead of manually writing hard functions, o

I read the argument in the article as something like “strong advanced type systems like Haskell’s are good because instead of manually writing hard functions, one can just write the type (ie the meaning of the function) and do a bunch of menial compiler-directed work to build up one’s function in little steps. This is great because one doesn’t need to “actually” write such horrible functions. I find it slightly silly because one still has to read such functions so it is still hard to know that they do the right thing. For example, consider the function in the article which has type: Sem (State s ': r) a -> S.StateT s (Sem r) a It seems pretty obvious what this morally should do. In some cases it is possible for polymorphism to force a value of a certain type to always behave a certain way. E.g. a value of type [a] must be the empty list because that is the only value with that type. On the other hand there are multiple values of type [[a]] (I.e. an empty list or an infinite list of empty lists or anything in between). A more complicated example is that the only thing a function with the signature of compose ((b -> c) -> (a -> b) -> (a -> c)) can do is compose functions whereas a function of type (Int-> Int) -> (Int-> Int) -> (Int -> Int) can do just about anything. Outside of abstract Haskell libraries, code tends to look more like the second case than the first. In this case it is hard to be sure that the function must behave in the correct way because of its type. I think it hinges on whether it is possible for Put to change the type of the state. If it can then types force you to always take the newly put value and return it with Get, otherwise it would be possible for Put to eg only sometimes work. So if one has to check that the code is correct, one must either read very carefully and check the code, or one must very carefully read the type signature and deduce that the code is correct. In the first case the fact that the compiler made the code easy to write doesn’t really help much. Perl5 taught us that just because a program was easy to write it does not mean it will be easy to read/check. In the second case, why do we have a program at all? If there is only one correct program we could have written then it seems to me that the program is in fact the type and the compiler ought to have been more clever and written it itself. (There are of course plenty of issues with that statement). It seems to me that claiming “Haskell is great because it helps automatically write difficult functions which are impossible to check” or “Haskell is great because it makes me do the manual steps in writing a function that can only ever do one thing and mixes that pointless code in with the thing I care about” is a bit silly. This all being said, I do think holes are a useful feature but I don’t think they are useful for entirely writing a function for you. They are particularly useful in proof assistants like Agda where one must manually exhibit a million trivial propositions and holes help fill in all the boring gaps. Agda doesn’t really suffer from the “multiple things a type could mean” issue.