[Haskell-cafe] Wow Monads!

[Joachim Durchholz]

Am 18.04.2017 um 23:33 schrieb Sergiu Ivanov:
> Haskell or OCaml type systems are usually not used for writing such
> exact specifications, because they are not expressive enough.

I have read statements that Haskell code still tends to "just work as 
expected and intended", and see that attributed to the type system.

Seemed to be related to Haskells expressivity, with the type system 
pretty much preventing the typical errors that people make.

So the sentiment was that it's not the same but close enough to be the 
same in practice. Though I doubt that that will hold up once you get 
more proficient in Haskell and start tackling really complicated things 
- but "simple stuff in Haskell" tends to get you farther than anybody 
would expect, so it's still a net win.
Just impressions though, I never had an opportunity to delve that deeply 
into Haskell.

 > Thus, in
> general, showing that Haskell or OCaml code typechecks is weaker than
> proving that it has a certain property (like not failing).

That a code type checks in Haskell still gives you a whole lot of 
guarantees. Such as "it doesn't have IO in the type signature so there 
cannot be any side effect deep inside".
(Ironically, people instantly started investigating ways to work around 
that. Still, the sort-of globals you can introduce via the State monad 
are still better-controlled than the globals in any other language.)

(Aside note: I don't know enough about OCaml to talk about its 
properties, but I do believe that they are much weaker than in Haskell.)

 > (However,
> passing Haskell or OCaml type checks is still stronger than passing Java
> type checks.)

Yep.

>> And I think you can trace that to the need to interface with the real
>> world.
>
> I have the same gut feeling.

I think interfacing with the outside world (still not "real" but just 
bits inside the operating system and on disk) is one major source of 
unreliability, but not the only one, and not necessarily the primary one.
YMMV.