what a fascinating name choice. I can’t read F* w/o immediately thinking someone is swearing
I feel the need to re-iterate what I wrote, which usually isn’t a good sign. You either misunderstood me or I misunderstand your reply.
To me, in my daily practice of programming Haskell, it is obvious that not being able to call IO
from non-IO is not what purity is about. It’s only the most prominent example.
What I want to highlight is that I can use any kind of type (quite often that type is monad) and put restrictions on the allowed code.
“Well that’s just strict typing, not purity”
… going back to the entire point of my comment that Haskell is not only about strict typing but it encourages the programmer to think about types and sensible invariants of the domain in which they are solving a problem, my liberal interpretation of the “worst practices should be hard” blogpost.
The purity is at the core of this feature because Haskell is designed to facilitate separation of IO and non-IO, or my-custom-complicated-monad-stack and some arithmetic of type Int -> Int
, this type and not-this-type. Where “this type” is not just a primitive like in C but domain specific.
Hoping to clear things up with this without coming across preachy or anything.