DEV Community

Discussion on: Types as propositions, programs as proofs

Collapse
 
rrampage profile image
Raunak Ramakrishnan

In Java, there are checked exceptions and unchecked exceptions. Checked ones can be caught in the code, unchecked ones like the ArrayOutOfBounds result in a Runtime exception. Runtime exceptions do not have to be caught i.e code will compile fine if you ignore them. OTOH, checked exceptions have to be caught.

You are right in that I had not considered global variables. I was thinking that they can also be added to the type signature
f = ((p and s) or e) -> ((q and s) or e) where s is all state variables. But I can see that there is too much pollution occurring with these additions.

Regarding functional languages like Haskell, how do they handle fatal errors like machine getting out of memory or being sent a kill -9 signal? Is that also built into the type system?

Finally, is there any book you can recommend for getting better at Functional programming? I tried Learn You a Haskell but after 5 chapters I kind of never got back into it.

Now you're thinking with Monads :-)

I'll need to learn FP to understand what that means :)

Thread Thread
 
drbearhands profile image
DrBearhands

I was thinking that they can also be added to the type signature [...]

Sure! That's what you would do in declarative languages.

Regarding functional languages like Haskell, how do they handle fatal errors like machine getting out of memory or being sent a kill -9 signal? Is that also built into the type system?

The functional part of a program is just declarations, so it doesn't really 'run'. Because of this it can't run out of memory or be interrupted either. That all happens in the runtime, IO Monad, or similar imperative structure, which can indeed crash in the ways you mentioned.

If the entire system were purely functional it'd be a different story, but I'm not aware of such systems existing in reality.

I'll need to learn FP to understand what that means :)

You seem to have the right mindset to apply FP in practice. Learning the formal definition of a Monad can wait a bit. I have a post planned for it in the future.

is there any book you can recommend for getting better at Functional programming?

Unfortunately no, I personally don't learn well from books at all. Most of my uni books were left unopened.

Learning Elm can be a good starting point, see the guide and the beginners' slack channel

Haskell and Idris certainly have more features, but those very same features can get in the way of understanding the basics. Their type systems for instance use more than just propositional logic (another subject for the future).