O'Reilly logo

Good Math by Mark C. Chu-Carroll

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

Prove It!

images/_pragprog/svg-0047.png

The grammar defines the syntax of valid types, but that’s not quite enough to make the types meaningful. Using that grammar, you can create type expressions that are valid but for which you can’t actually write an expression that will produce a value of that type. When there is an expression that has a type, we say that the expression inhabits the type and that the type is an inhabited type. If there is no expression that can inhabit a type, we say it’s uninhabitable. So what’s the difference between an inhabitable type and an uninhabitable type?

The answer comes from something called the Curry-Howard isomorphism. The Curry-Howard ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required