Skip to main content
Tweeted twitter.com/#!/StackCSTheory/status/461745590758805504
Corrected typo and added link.
Source Link
Martin Berger
  • 11.6k
  • 3
  • 40
  • 71

I am currently reading the book Programming in Martin-Löf type thoeryProgramming in Martin-Löf type theory by Nordström et al. In the book they have two important parts, one about monomorphic set theory and the other about polymorphic set theory. Why do they do this? What are important differences. As far as I understand from the book monomorphic version reduces to polymorphic but not vice versa. Why is this so?

I am currently reading the book Programming in Martin-Löf type thoery by Nordström et al. In the book they have two important parts, one about monomorphic set theory and the other about polymorphic set theory. Why do they do this? What are important differences. As far as I understand from the book monomorphic version reduces to polymorphic but not vice versa. Why is this so?

I am currently reading the book Programming in Martin-Löf type theory by Nordström et al. In the book they have two important parts, one about monomorphic set theory and the other about polymorphic set theory. Why do they do this? What are important differences. As far as I understand from the book monomorphic version reduces to polymorphic but not vice versa. Why is this so?

Source Link

Monomorphic vs Polymorphic type theory

I am currently reading the book Programming in Martin-Löf type thoery by Nordström et al. In the book they have two important parts, one about monomorphic set theory and the other about polymorphic set theory. Why do they do this? What are important differences. As far as I understand from the book monomorphic version reduces to polymorphic but not vice versa. Why is this so?