[Haskell-cafe] Wow Monads!

[Sergiu Ivanov]

Thus quoth  Joachim Durchholz  at 07:51 on Wed, Apr 19 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.
[...]
> So the sentiment was that it's not the same but close enough to be the
> same in practice.

Sure, this "close enough" bit is one of the things which make Haskell
very attractive.

Now, it's not "close enough" for critical systems (satellites, nuclear
reactors, etc.), from what I know.

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

I tend to see Haskell's type system as very restrictive and only
allowing behaviour which composes well.  It's also rich enough to allow
specification of quite a wide variety of behaviour.

However, there are a couple big "backdoors", like the IO monad.
Typechecking gives zero guarantees for functions of type IO (), for
example.

> Though I doubt that that will hold up once you get more proficient in
> Haskell and start tackling really complicated things

To me, it really depends on the kind of complicated things.  If you
manage to explain the thing at the type level, then typechecking may
give you pretty strong guarantees.  I'm thinking of parsing and
concurrency as positive examples and exception handling as a somewhat
negative example.

> but "simple stuff in Haskell" tends to get you farther than anybody
> would expect, so it's still a net win.

Absolutely.

>> 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".

Right, of course.

> (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.)

In fact, I believe having pure functions does not so much target
removing state as it does making the state _explicit_.  Thus, the State
monad is not a work-around to purity, it's a way of purely describing
state.

And then, if the State monad is too lax for one's purposes, one can use
Applicative or even define more specific typeclasses.

> (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.)

That's what I tend to believe as well from looking over people's
shoulders.

>>> 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.

Yes, that unreliability comes with crossing the frontier between
theoretical and applied computer sciences (that's an imprecise
metaphor :-) )

--
Sergiu
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 487 bytes
Desc: not available
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20170419/94bad84a/attachment.sig>