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

[Jonas Scholl]

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



-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 473 bytes
Desc: OpenPGP digital signature
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20150810/ce281039/attachment.sig>