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

[Tom Ellis]

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.