
On Dec 16, 2019, at 2:32 AM, Tom Ellis
wrote: These examples illustrate the difference in pattern matching between types defined by data and newtype:
(\ (N True) -> True) ⊥ ⇒ ⊥ (\ (D True) -> True) ⊥ ⇒ ⊥ (\ ~(D True) -> True) ⊥ ⇒ True
Additional examples may be found in Section 4.2.3.
But unlike the examples in 4.2.3, which do show differences between "newtype" and "data", the above does not seem to show any actual difference. For that the pattern after the constructor would I believe have to be irrefutable, which "True" is not.
I think what you're saying is that this doesn't show a difference because
(\ ~(N True) -> True) ⊥ ⇒ True
Yes, because of that, and also because even if it were otherwise, it is not one of the examples. :-( But indeed the expressions used in the examples behave indistinguishably for "N" and "D". So the examples don't seem to make the intended point. -- Viktor.