Type Systems and Logic

Type Systems and Logic(codewords.recurse.com)

5 points by zeronone 9 years ago | 1 comment

> Hindley-Milner type systems – which I here use to refer broadly to type systems like those used by Haskell and OCaml – correspond to propositional logic.

Is this true? HM type systems at least have a limited form of universal quantification (type schemes), which means we're dealing with predicate calculus, not propositional logic.

tree_of_item 9 years ago |

> Hindley-Milner type systems – which I here use to refer broadly to type systems like those used by Haskell and OCaml – correspond to propositional logic.

Is this true? HM type systems at least have a limited form of universal quantification (type schemes), which means we're dealing with predicate calculus, not propositional logic.