[Haskell-cafe] Wow Monads!
jo at durchholz.org
Wed Apr 19 07:51:47 UTC 2017
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
> 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.)
> passing Haskell or OCaml type checks is still stronger than passing Java
> type checks.)
>> And I think you can trace that to the need to interface with the real
> 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.
More information about the Haskell-Cafe