Prove It!
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 ...
Get Good Math now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.
