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

[Jonas Scholl]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA256

Of course... my mistake. And now we also have mkNs 5 n == mkNs 5 (id2
n), without any lazy pattern matching. But we still have mkDs 5 d ==
_|_, so N and D still have different semantics.

On 08/10/2015 03:56 PM, amindfv at gmail.com wrote:
> 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

-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2

iQEcBAEBCAAGBQJVyOUvAAoJEM0PYZBmfhoBXnIIALpMHC8BHMN5EgKREFQfsX6k
dhyhOxaxDxHM7gYcgxKo5il2rtDJT5sNjuzeyBfBpxKqmjg1YSLEsB3E2fGC8JZV
LOBCROAqbcmAXRPNAKdbMaT8XYaLrMqFkqWpcNjxe752RAbqgbb9II1O7GLKYSDZ
Q3cEIvBRBHcfeQKQRHnbunXdrdojRZf9LdSbm/HkzatPdToAMUsTdhNAPRhnxM5R
EHP2uhmtwRzEcCZ+/tzeJ/OYltqZ9hJ419CwwJs8z9hJUprLpdK4HS76IvDde3kq
wFUWqzpESAgOxrtp6lTwLFSsOsXyg3PM4x0+F27sA/z+ls6GrvYM+VcXa4XMBlU=
=jkjF
-----END PGP SIGNATURE-----