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

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