Theoretically: the Curry-Howard isomorphism gives us an interpretation of this type as the "false" proposition. "false" is useful as a proposition on its own; but is also useful for constructing the "not" combinator (as type Not a = a -> False
) and other similar constructions.
Pragmatically: this type can be used to prevent certain branches of parameterized data types from coming into existence. For example, I've used this in a library for parsing various game trees something like this:
data RuleSet a = Known !a | Unknown String
data GoRuleChoices = Japanese | Chinese
data LinesOfActionChoices -- there are none in the spec!
type GoRuleSet = RuleSet GoRuleChoices
type LinesOfActionRuleSet = RuleSet LinesOfActionChoices
The impact of this is that, when parsing a Lines of Action game tree, if there's a ruleset specified, we know its constructor will be Unknown
, and can leave other branches off during pattern matches, etc.
与恶龙缠斗过久,自身亦成为恶龙;凝视深渊过久,深渊将回以凝视…