re: Types as propositions, programs as proofs VIEW POST


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

code of conduct - report abuse