Re: [Haskell-cafe] an idea for modifiyng data/newtype syntax: use `::=` instead of `=`

There is still a difference between a data type with one strict field and a newtype: You can strip the constructor of a newtype without evaluating anything. Suppose we have data D = D !D data N = N N d :: D d = D d n :: N n = N n d and n both evaluate to bottom, but it is possible to pattern match on (N t) and succeed, while matching on (D t) does not. Example: mkDs :: Int -> D -> String mkDs i (D t) | i <= 0 = [] | otherwise = 'd' : mkDs (i - 1) t mkNs :: Int -> N -> String mkNs i (N t) | i <= 0 = [] | otherwise = 'n' : mkNs (i - 1) t Evaluating mkNs 5 n returns "nnnnn", while evaluating mkDs 5 d loops forever. Now we can define: f :: D -> N f (D t) = N (f t) g :: N -> D g (N t) = D (g t) id1 :: D -> D id1 = g . f id2 :: N -> N id2 = f . g If both representations should be equal, we should get that mkNs 5 n == mkNs 5 (id2 n). But id2 converts everything to the D type first, which is only inhabited by _|_, and then pattern matches on it. So we get "nnnnn" == _|_, which is obviously false. If we change f to use a lazy pattern match, the equality holds again. So D and N are maybe equivalent if we allow only lazy pattern matches on D. As this is not the case, the two are clearly not equivalent. On 08/09/2015 11:10 PM, Tom Ellis wrote:

On Sun, Aug 09, 2015 at 07:49:10PM +0200, MigMit wrote:

...

You know, you've kinda conviced me.

I hope I'm correct then!

...

The difference between strict and non-strict parameters is in how constructors work. "data D = D Int" is still the same as "data D = D !Int", but it's constructor — as a function — is more restricted. It's somewhat like defining "d n = D $! n", and then not exporting D, but only d.

Right.

...

That said, it might be true that semantics differ depending on what is exported. So, it might be true that your D has the same semantics as N. We still can distinguish between those using various unsafe* hacks — but those are what they are: hacks.

Отправлено с iPad

...

9 авг. 2015 г., в 13:35, Tom Ellis написал(а):

On the contrary, it *is* the same thing

Prelude> data D = D !Int deriving Show Prelude> D undefined *** Exception: Prelude.undefined Prelude> undefined :: D *** Exception: Prelude.undefined

...

On Sun, Aug 09, 2015 at 01:30:01PM +0200, MigMit wrote: First, the half that I agree with: f . g = id. No doubt.

But g . f > id. And the value "d" that you want is "undefined". g (f undefined) = D undefined, which is not the same as (undefined :: D).

Отправлено с iPad

...

...

9 авг. 2015 г., в 13:17, Tom Ellis написал(а):

On Sun, Aug 09, 2015 at 01:09:21PM +0200, MigMit wrote: I disagree.

Ah, good. A concrete point of disagreement. What, then, is wrong with the solution

f :: D -> N f (D t) = N t

g :: N -> D g (N t) = D t

If you disagree that `f . g = id` and `g . f = id` then you must be able to find

* a type `T`

and either

* `n :: N` such that `f (g n)` does not denote the same thing as `n`

or

* `d :: D` such that `g (f d)` does not denote the same thing as `d`

Can you?

Tom

...

> 9 авг. 2015 г., в 12:37, Tom Ellis написал(а): > On Sun, Aug 09, 2015 at 12:15:47PM +0200, MigMit wrote: >>> Right, you can distinguish data declarations from newtype declarations this >>> way, but by using Template Haskell you can also distinguish >>> >>> * data A = A Int >>> * data A = A { a :: Int } >>> * data A = A' Int >>> * data A = A Int !(), and >>> * newtype B = B A (where A has one of the above definitions) >> >> Sure, because they are different. >> >>> from each other. My claim is that >>> >>> * data B = B !A >>> >>> is as indistinguishable from the above four as they are from each other. >> >> Can you please NOT say that some thing can be distinguished AND that they >> are indistinguishable in the same post? > > I think we are perhaps talking at cross purposes. > > To clarify, here is an explicit statement (somewhat weaker than the full > generality of my claim): > > `data D = D !T` and `newtype N = N T` are isomorphic in the sense that > there exist `f :: D -> N` and `g :: N -> D` such that `f . g = id` and > `g . f = id`. > > Do you agree or disagree with this statement? Then we may proceed.

---

Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

---

Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

---

Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe