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

Tom Ellis tom-lists-haskell-cafe-2013 at jaguarpaw.co.uk
Mon Aug 10 22:47:00 UTC 2015


I'm not claiming that they should behave the same with regard to the
*syntax* of case analysis (NB case analysis of newtypes is already treated
specially since the constructor doesn't actually exist).

Again I refer interested parties to my proposed translation between the two
methods of defining types:

    http://stackoverflow.com/posts/21331284/revisions

Does this answer your objection?

Tom


On Mon, Aug 10, 2015 at 01:38:23PM +0200, Jonas Scholl wrote:
> 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
> > 
> 
> 
> 



> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe



More information about the Haskell-Cafe mailing list