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

[MigMit]

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 <tom-lists-haskell-cafe-2013 at jaguarpaw.co.uk> написал(а):
> 
>> 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 <tom-lists-haskell-cafe-2013 at jaguarpaw.co.uk> написал(а):
>>> 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 at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe