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

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