23 Oct 1996
The objective of the proposal is to support pattern matching in the context of abstract datatype. Run-time overheads should be minimal. In particular, it should be possible for a compiler to implement views in such a way that, in the case where the concrete representation and the view defined for pattern matching are isomorphic, no additional run time costs are introduced because a program makes use of data abstraction. Values with viewtypes are constructed only at the time when pattern matching is applied to the resulting value, making it possible to completely optimize away the actual construction in simple cases such as this. Some problems (or at least complications) with previous proposals for views and Miranda laws are avoided by providing view transformations in only one direction. Views may be used in pattern matching but not in the construction of values. Hence, pattern matching with views should be considered a syntactic bundling of case selection and component extraction, rather than a syntactic mechanism for inverting construction. Since ordinary functions can be used to construct values having abstract datatypes, this is not a problem. An added advantage of this approach is that views may be used to capture some but not all the information that a value contains. The proposal is given in the form of changes to the Haskell 1.4 definition. Following the proposal is some additional discussion with additional examples. You may want to look at some of the examples before reading the proposal proper.
topdecl ->
view [context =>] simpletype of type = constrs where valdefs
4. (d) Matching a non- _|_ value against a pattern whose outermost component is a constructor defined by view proceeds as follows. First, the view transformation for the view of the constructor is applied to the value. If the result is _|_, then the matching diverges. If the result was created by a different view constructor then matching fails. If the constructors are the same, the result of the match is the result of matching the sub-patterns left-to-right against the components of the value produced by the view transformation: if all matches succeed, the overall match succeeds; the first to fail or diverge causes the overall match to fail or diverge, respectively.
Change rules (m) and (n) by replacing "K" with "X".
Change rule (g) by replacing "K" with "Y". (I think this correct an existing error in rule (k).)
Add the following two rules:
(r) case v of { W x1 ... xn -> e; _ -> e' } = e'
where W and W', of arity n and m respectively, are distinct view
constructors for a view with view transformation f; and
f v = W' e1 ... em
(s) case v of { W x1 ... xn -> e; _ -> e' }
= case e1 of { x'1 -> ... case en of { x'n -> e[x'1/x1 ...
x'n/xn] }...}
where x'1 ... x'n are completely new variables;
W, of arity n, is a view constructors for a view with view
transformation f; and
f v = W e1 ... en
topdecl ->
view [context =>] simpletype of type = constrs where valdefs
Views are intended to support pattern matching in the concept of abstract datatypes. Whenever a constructor defined in a view declaration is used in a pattern, the value being matched is automatically transformed into the view type. View transformations are not reversible. In fact, view types can be considered to be virtual types, since no value having a view type need ever be constructed. Restrictions given below insure that values with viewtypes are constructed only at the time when pattern matching is applied to the resulting value, making it possible to optimize away the actual construction in simple cases.
In a view declaration of the form
view c => s of t = k where dis equivalent to
data c => s = k dand is valid if and only if d defines (only) a suitably named function of type c => t -> s and the restrictions and scoping rules given below are satisfied. We call s a viewtype and informally use the name of the type constructor introduced in s as the name of the view. The type t is called the actual type of the view. The function defined in d is called a view transformation. The constructors defined in a view declaration are called view constructors. The name of a view transformation must be identical to the name of the view except the first character of the name must be changed from upper case to lower case. The scope of the name of the view transformation is d. The same name may be used outside d without conflict. We may think of the compiler giving the view transformation a new name that is unknown to the programmer, so the view transformation may never be called explicitly or redefined. As dictated by the semantics of pattern matching, calls to the now anonymous view transformation will be inserted, as necessary, into a program. Example: The Natural view can be used to provide an alternative to (n+1) patterns.
view (Integral a) => Natural a of a = Zero | Succ a
where
natural 0 = Zero
natural n
| n > 0 = Succ (n-1)
| otherwise
= error "Natural: Natural view excludes negative values"
Patterns with different viewtypes may be matched against the same value
provided all of the viewtypes correspond to a common actual type.
factorial :: (Integral a) => a -> a factorial Zero = 1 factorial (n@Succ m) = n * factorial mIn the second equation defining factorial, the same value is matched against both a pattern, Succ m, having a viewtype, Natural a, and a pattern, n, of the actual type, a.
Views cannot be used to define (n+k) patterns for arbitrary k, but additional views may be defined to support a fixed number of view constructors: Succ2, Succ3, Succ4, ....
view c => s of t = k where d
Despite restriction 2, constructors of k may be passed to polymorphic functions called from within d, but again it is possible only to return any computed value of type s.
Note: Item 2 implies that newtypes are a form of algebraic datatype, which does not agree with the use of the term in sections 3.17.3 and 4.2.
let C y = C x in ydid not always return a value equal to x. Phil's paper contains an example with polar coordinates. Near the end of the paper, Phil says, "the polar view of complex numbers ... is valid only if for all angles t1 and t2 the equation
Pole 0 t1 = Pole 0 t2is consistent with the rest of the program", since all complex number with 0 magnitude will have the same actual (Cartesian) representation. A similar problem existed with laws in Miranda, and resulted in their removal.
We solve this problem by making the equation
let C y = C x in ysyntactically invalid! The use of a view constructor C on the right side of the above equation is not valid.
Equational reasoning with views is now straight forward. View transformations may be freely added when required in order to perform pattern matching. The is, the equational reasoner may perform the same transformations that are specified in rules (r) and (s) of the formal semantics of pattern matching. If such transformations are omitted, or introduced where they should not be, the result is simply an expression that cannot be reduced. No incorrect conclusion can be drawn.
We propose that view transformations inserted into a program during equational reasoning be enclosed in distinctive comment brackets so code remains valid.
For example, with the Natural view defined above and the function
succ n = n + 1we could reason as follows:
let Succ y = succ x in y
== let Succ y = x + 1 in y
== let Succ y = {-> natural <-} (x + 1) in y
== let y = x + 1 - 1 in y, when x + 1 > 0
== x, when x + 1 > 0 and x + 1 is valid
This makes it clear that the above transformation works only when x is
nonnegative and x + 1 is valid (e.g. does not overflow).
Module ComplexViews (Cmplx, pole, Polar(Pole)) where
data Cmplx = MkPole Float Float
pole rho theta = MkPole rho theta
view Polar of Cmplx = Pole Float Float where
polar (MkPole rho theta) = Pole rho theta
Since a value having a viewtype is created by a view transformation only
when the value is being matched against a pattern based on the viewtype, it
is likely that a compiler can avoid the construction of the value with the
viewtype and implement Cmplx as efficiently as would be possible if views
were not being used, provided the view transformation is know at compile
time. This suggests that view transformations might be included in
implementation dependent interface files. In some cases, for example when
view transformations are recursive, optimizations like this may not be
possible.
We can modify the above module to use a cartesian representation while preserving the polar view.
Module ComplexViews (Cmplx, pole, Polar(Pole)) where
data Cmplx = MkCmplx Float Float
-- The following implement a cartesian representation.
pole rho theta = MkCmplx (rho * cos theta) (rho * sin theta)
view Polar of Cmplx = Pole Float Float where
polar (MkCmplx x y) = Pole (sqrt(x*x+y*y)) (atan2 y x)
With the earlier implementation,
Pole r2 t2 = pole r1 t1would have been equivalent to
r2 = r1 t2 = t1This is not the case with the second implementation, due to normalization of the angle and minor numerical differences that may be generated during transformations from polar to cartesian coordinates and back again. If we allowed the function "pole", which effectively transforms polar values out of the view, to have the name "Pole", we could have written
Pole r2 t2 = Pole r1 t1instead of
Pole r2 t2 = pole r1 t1which would have been very misleading. The fact that the names "Pole" and "pole" differ serves as a warning to the programmer that they need not be quite the same. That is, the pattern matching need not exactly reverse the construction.
With a bit more work we can allow polar and cartesian representations and views to be freely mixed.
Module ComplexViews (PoleRep, CartRep,
pole, cart,
Polar(Pole), Cartesian(Cart)
CmplxClass)
where
data PoleRep = MkPole Float Float
data CartRep = MkCart Float Float
class CmplxClass a where
get_rho :: a -> Float
get_theta :: a -> Float
get_x :: a -> Float
get_y :: a -> Float
instance CmplxClass PoleRep where
get_rho (MkPole rho theta) = rho
get_theta (MkPole rho theta) = theta
get_x (MkPole rho theta) = rho * cos theta
get_y (MkPole rho theta) = rho * sin theta
instance CmplxClass CartRep where
get_rho (MkCart x y) = sqrt(x*x+y*y)
get_theta (MkCart x y) = atan2 y x
get_x (MkCart x y) = x
get_y (MkCart x y) = y
view (CmplxClass a) => Polar of a = Pole Float Float where
polar a = Pole (get_rho a) (get_theta a)
view (CmplxClass a) => Cartesian of a = Cart Float Float where
cartesian a = Cart (get_x a) (get_y a)
pole rho theta = MkPole rho theta
cart x y = MkCart x y
The members of the CmplxClass class have not been exported, so additional
representations for complex numbers cannot be introduced outside this
module.
Examples of a few representation independent functions that can be written with this implementation of complex numbers follow.
toPole :: (CmplxClass a) => a -> PoleRep toPole (Pole x y) = pole x y -- toCart is similar addComplex :: (CmplxClass a, CmplxClass b) => a -> b -> CartRep addComplex (Cart x1 y1) (Cart x2 y2) = cart (x1 + x2) (y1 + y2) multComplex :: (CmplxClass a, CmplxClass b) => a -> b -> PoleRep multComplex (Pole r1 t1) (Pole r2 t2) = pole (r1 * r2) (t1 + t2)
A backwards view of lists is defined by the following view, which uses the view being defined within the definition of the view transformation. This will result in a recursive call to the view transformation, backwards.
view Backwards a of [a] = [a] `Snoc` a | Nil
where
backwards [] = Nil
backwards (x:[]) = [] `Snoc` x
backwards (x1:(xs `Snoc` xn)) = (x1:xs) `Snoc` xn
In a variation of the above, the view being defined may be used in a
pattern within a where clause.
view Backwards2 a of [a] = [a] `Snoc2` a | Nil2
where
backwards2 [] = Nil
backwards2 (x:[]) = [] `Snoc2` x
backwards2 (x1:ys) = (x1:xs) `Snoc2` xn where (xs `Snoc2` xn) = ys
Finally, direct recursion is allowed, but probably not very useful in
realistic examples.
view Last a of [a] = Last a
where
last [a] = Last a
last (x:xs) = last xs
final [] = error "final: not defined for []" final (Last x) = xHowever, if we had written the two equations in the other order
final (Last x) = x final [] = error "final: not defined for []"then the error message returned whenever (final []) is evaluated would not be the one given in the bottom equation, since the view function will be called when an attempt is made to use the first equation.
In general, it is a good idea to make all view transformations total, particularly if different views are likely to be used together.
Haskell 1.4 allows selective export of constructors; using a dummy constructor that is not exported for cases where pattern matching should fail may be useful.
The following module supports (n+k) pattern matching for values of k up to 4 and allows Succ1 as an alternative to Succ. In addition, rather than producing an error message when an inappropriate case occurs, these views allow pattern matching to fail so a programmer can catch errors.
Module Naturals (Natural(Zero, Succ),
Natural1(Succ1),
Natural2(Succ2),
Natural3(Succ3),
Natural4(Succ4)
)
view (Integral a) => Natural a of a = Zero | Succ a | FailNatural
where
natural 0 = Zero
natural n
| n >= 1 = Succ (n-1)
| otherwise = FailNatural
view (Integral a) => Natural1 a of a = Succ1 a | FailNatural1
where
natural1 n
| n >= 1 = Succ1 (n-1)
| otherwise = FailNatural1
view (Integral a) => Natural2 a of a = Succ2 a | FailNatural2
where
natural2 n
| n >= 2 = Succ2 (n-2)
| otherwise = FailNatural2
view (Integral a) => Natural3 a of a = Succ3 a | FailNatural3
where
natural3 n
| n >= 3 = Succ3 (n-3)
| otherwise = FailNatural3
view (Integral a) => Natural4 a of a = Succ4 a | FailNatural4
where
natural4 n
| n >= 4 = Succ4 (n-4)
| otherwise = FailNatural4
We can now write:
fib Zero = 1 fib (Succ Zero) = 1 fib (Succ2 m)@(Succ1 n) = fib m + fib n fib _ = error "My error message"The first three lines of the definition of fib may be reorder in any way without changing the meaning. (Okay, I admit it. This example is a bit contrived.)
Consider the following views.
view Sign of Int = Negative | Naught | Positive
where
sign n | n < 0 = Negative
| n == 0 = Naught
| n > 0 = Positive
view Parity of Int = Odd | Even
where
parity n | odd n = Odd
| otherwise = Even
Notice that both view transformations are total.
Using these we can write
absol n@Negative = -n absol Naught = 0 absol n@Positive = nand
power 0.0 Naught = error "0.0 to the 0 power is undefined" power _ Naught = 1.0 power x n@Negative = 1/power x (-n) power x n@Odd = x * y * y where y = power (n `div` 2) x power x n@Even = y * y where y = power (n `div` 2) xIn the definition of power, notice that two different views are used in order to cover all of the interesting cases. The view transformations are total, so problems with partial views are avoided. In both function definitions, the "guard" is moved to the parameter being tested. This approach does not work if a guard is being used to test for a relationship between the values of several paramenter.
data JoinList a = Nil | Unit a | JoinList a `Join` JoinList a
class OrderContainer cont where
isEmpty :: cont a -> Bool
first :: cont a -> a
rest :: cont a -> cont a
view (OrderContainer cont) =>
List a of cont a = Empty | a `Cons` (cont a)
where
list xs = if isEmpty xs then Empty
else (first a) `Cons` (rest a)
instance OrderContainer [] where
isEmpty [] = True
isEmpty (x:xs) = False
first (x:xs) = x
rest (x:xs) = xs
instance OrderContainer JoinList where
isEmpty Nil = True
isEmpty (Unit x) = False
isEmpty (xs `Join` ys) = isEmpty xs && isEmpty ys
first (Unit x) = x
first (xs `Join` ys) = if isEmpty xs then first ys
else first xs
rest (Unit x) = Nil
rest (xs `Join` ys) = if isEmpty xs then rest ys
else rest xs `Join` ys
Perhaps a more appropriate solution to the supporting a list view of
"JoinList" is to define
class (MonadPlus m) => OrderContainer m where
null :: m a -> Bool
head :: m a -> a
tail :: m a -> m a
allowing a variety of container types to be processed by overloaded
functions. The details are left to the reader.
[2] Pedro, P. G., Pena, R. and Nunez, M., "A new look at mattern matching in abstract types." ICFP (1996), 110-121.
[3] Wadler, P., "Views: A way for pattern matching to cohabit with data abstraction", POPL 14 (1987), 307-313.