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

[amindfv at gmail.com]

El Aug 10, 2015, a las 7:38, Jonas Scholl <anselm.scholl at tu-harburg.de> escribió:

> 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
> 

This should be "newtype N = N N", no?

Tom

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