Alleged problems with equational reasoning caused by views

[Arie Peterson]

J. Garrett Morris wrote (to Bulat Ziganshin):

> Yes - you've reiterated Wadler's original design, with an automatic
> creation of a type class.  Erwig and Peyton-Jones, _Pattern Guards and
> Transformational Patterns_
> (http://research.microsoft.com/~simonpj/Papers/pat.htm) mentions
> problems with equational reasoning raised by this approach.

I just read this paper, in particular the part about the problems with
equational reasoning that come up once you introduce (a certain form of)
views.

I fail to appreciate those problems. Perhaps someone can help me see them?
:-)

### Polar representation

Before taking on the problematic 'Half', I review the earlier example of
the polar representation of complex numbers.

> data Complex = Cart Float Float
>
> view Polar of Complex = Polar Float Float where
>   polar (Cart r i) = Polar (sqrt(r*r+i*i)) (atan2 r i)

I am slightly puzzled by this notation: the role of the extra function (?)
'polar' is unclear to me. If I leave it out, the definition makes sense:

  'Cart r i' and 'Polar (sqrt(r*r+i*i)) (atan2 r i)' are declared to be
the same object.

Note that this definition provides only one direction of the "change of
coordinates": if we define a complex number by giving its polar
representation, then its cartesian components are not yet well defined.

This means that the "constructor" 'Polar' is not a well defined function,
unless you assume a new datatype 'Polar' (of "complex numbers in polar
representation") and have 'Polar :: Float -> Float -> Polar'. This is what
the proposal seems to do, but I find it very misleading: if you look at
the defining equation of the view, the constructor 'Polar' takes two
floating point numbers, and returns a complex number: 'Polar :: Float ->
Float -> Complex'.
(Said another way: when 'Polar' appears in a pattern, it must convert the
original cartesian coordinates to polar ones; when it appears in an
expression, it converts polar back to cartesian. The view given above only
allows the first of these two.)
(Maybe this is where the proposal strays from the natural "equational"
meaning?)


### 'Half'

OK, now we consider the following view:

> view Half of Int = Half Int where
>   half i = Half (i `div` 2)

Again, I propose to leave out the word 'half', and conclude that the
integer 'i' is declared to be equal to 'Half (i `div` 2)'.
(Maybe at this point my interpretation diverges from the intended meaning,
but then the first example does not implement the usual polar
representation of complex numbers.)

Just as before, we have not specified what number 'Half n' actually is;
even if we are consistent it could be either '2*n' or '2*n+1'.

Therefore, if we define the function 'f' by

> f (Half i) = i+1

, the only sensible way I can think of to compute 'f (Half 8)' is by
pattern matching 'Half 8' against 'Half i', giving the binding 'i -> 8',
and substituting this in the RHS of 'f', giving 'f (Half 8) = 8+1 = 9'. Of
course this is also what you get by "replacing equals for equals", as the
paper puts it.

The paper however continues to state that "'f (Half 8) = 9' [...] is not
true because 'f (Half 8) = 5' due to the computational part of 'Half'".
***I really don't see how one would conclude this.*** It would be strange
to divide the parameter of 'Half' by 2 -- 'n' is already half of the
number represented by 'Half n'.


Perhaps someone can enlighten me to see the problem. I have a feeling,
though, that there is no inherent problem with views, only some confusion
about which way the coordinate transformations should go.

In fact, I would love to see views in Haskell, but I'll save that
discussion for another thread.


Kind regards,

Arie