
Not sure where to post about this, and it has likely been noted elsewhere already, but reading through the report I see in Section 3.17.2
• Consider the following declarations:
newtype N = N Bool data D = D !Bool
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. Thus, e.g. the below (which duplicates 4.2.3) would do the job: (\ (N _) -> True) ⊥ ⇒ True (\ (D _) -> True) ⊥ ⇒ ⊥ Perhaps I misunderstood something, but if not, and this has not been noted before, it may be worth fixing in the next revision. -- Viktor.

On Mon, Dec 16, 2019 at 01:42:39AM -0500, Viktor Dukhovni wrote:
Not sure where to post about this, and it has likely been noted elsewhere already, but reading through the report I see in Section 3.17.2
• Consider the following declarations:
newtype N = N Bool data D = D !Bool
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

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.

On Mon, Dec 16, 2019 at 02:36:48AM -0500, Viktor Dukhovni wrote:
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
[...] 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.
I agree that's very strange!

On 2019-12-16 1:42 a.m., Viktor Dukhovni wrote:
Not sure where to post about this, and it has likely been noted elsewhere already, but reading through the report I see in Section 3.17.2
I'm not sure either, but one place you could report it is at https://github.com/haskell/rfcs/issues No guarantees, but it would make the issue slightly less likely to be forgotten.
• Consider the following declarations:
newtype N = N Bool data D = D !Bool
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.
Thus, e.g. the below (which duplicates 4.2.3) would do the job:
(\ (N _) -> True) ⊥ ⇒ True (\ (D _) -> True) ⊥ ⇒ ⊥
Perhaps I misunderstood something, but if not, and this has not been noted before, it may be worth fixing in the next revision.
participants (3)
-
Mario Blažević
-
Tom Ellis
-
Viktor Dukhovni