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