3 ms·
That books wants to build the foundation (dependent types) before making the big claim in chapter 3. It's a bit weird because has Haskell shows, you don't need
by lonelappde 7y ago
That books wants to build the foundation (dependent types) before making the big claim in chapter 3.
It's a bit weird because has Haskell shows, you don't need dependent types for basic theorem proving. (but dependent types do give a lot of useful power)
- dwohnitmok 7y agoWell if you just have Haskell 2010 types, you're talking about really really basic theorem proving since all you have is propositional logic. The most interesting thing I can think of to prove with Haskell 2010 types is (the constructive version of) de Morgan's laws. Almost all other interesting mathematical statements are out of reach.