A couple of people have asked about:
[2] W Burton, E Meijer, P Sansom, S Thompson, P Wadler, "A (sic) extension
to Haskell 1.3 for views", sent to the Haskell mailing list
23 Oct 1996
I am enclosing a copy of the "(sic)" proposal below. In light of Simon's
proposal, the "(sic)" proposal should now be seen as a source of examples,
rather than a still viable proposal.
I agree with Phil Wadler:
> I think Heribert Schuetz makes a good argument that Simon's
> proposed notation would work better if adapted to the Maybe monad.
> Simon's original proposal struck me as something of a hack,
> whereas Schuetz's variant seems more disciplined. -- P
I note that the "Maybe" approach allows nesting (via ++), which overcomes
even the fairly obscure advantage of views noted by Simon. It also appears
that the optimization of pattern-matching as given by Phil Wadler, in
Chapter 5 of "The Implementation of Functional Programming Languages", by
Simon Peyton Jones, can be easily expressed as a source to source
translation, if the Maybe monad is used.
On the other hand, given that we can hand translate all this into Haskell
1.4, I am also reasonable happy with Simon's original proposal (where the
Just's are not explicitly given). The original proposal handles the vast
majority of situations with less syntax.
Finally, a couple of people have wondered whether the new guard syntax
should be extended to other monads (perhaps with a now subclass with a
fromMonad operator). The generalization of list comprehensions was cited
as a precedent. Some members of the Haskell 1.4 Committee had second
thought about general monad comprehensions after we saw some of the
problems this caused. I don't think we want to generalize the guard
notation to monads other than Maybe. All we would get for our efforts are
additional obscure error messages, and we have enough of these already.
Warren
________________________________________________________________________
X-Sender: [EMAIL PROTECTED]
Mime-Version: 1.0
Date: Wed, 23 Oct 1996 12:41:54 -0700
To: [EMAIL PROTECTED]
From: [EMAIL PROTECTED] (F. Warren Burton)
Subject: Views in Haskell
Cc: [EMAIL PROTECTED], [EMAIL PROTECTED], [EMAIL PROTECTED],
[EMAIL PROTECTED], [EMAIL PROTECTED]
A proposal to extend Haskell 1.3 to support views follows. It is of course
too late to consider this as an addition to Haskell 1.3. (Furthermore,
with the addition of view it would be hard to justify continued support for
our beloved n+k patterns.) Hence, this should be considered a proposal for
a common extension to Haskell 1.3, or whatever John is currently calling
these things.
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.3 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.
________________________________________________________________________
A EXTENSION TO HASKELL 1.3 FOR VIEWS
Proposed by Warren Burton, Erik Meijer,
Patrick Sansom, Simon Thompson and Phil Wadler
SYNTAX
------
1. "view" is a reserved word.
2. The following production is added to the Haskell 1.3 context free
syntax:
topdecl ->
"view" [context =>] simpletype "of" type = constrs "where" valdefs
3.17.2 Informal Semantics of Pattern Matching (changes)
------ -------- --------- -- ------- --------
Add the following:
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.
3.17.3 Formal Semantics of Pattern Matching (changes)
------ ------ --------- -- ------- --------
Before "N is a newtype constructor" add "W and W' are view constructors; X
may be either a algebraic datatype (data) constructor or a view
constructor; Y may be either a algebraic datatype (data) constructor, a
newtype constructor or a view constructor;".
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
4.2 User-Defined Datatypes (revised wording to include viewtypes)
--- ------------ ---------
In this section, we will describe algebraic datatypes (data declarations),
renamed datatypes (newtype declarations), type synonyms (type
declarations), and viewtypes (view declarations). These declarations may
only appear at the top level of a module.
4.2.4 View Declarations (new section)
----- ---- ------------
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 d
is equivalent to
data c => s = k
d
and 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 m
In 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, ....
Restrictions and Scoping Rules
------------ --- ------- -----
The following restrictions refer to the components of a view declaration of
the form:
view c => s of t = k where d
1. Viewtypes may not be recursive.
2. Outside of d, the constructors and field labels defined in k may be
used only in patterns and in import and export lists.
3. Within d, field labels may not be used as selector functions or in
updates. However, within d, the constructors and field labels defined in k
may be used to construct a value of type s.
4. Aside from the defining occurrence, the type constructor of s (i.e. the
view name) may be used only in import and export lists. In particular,
nothing may be declared to have a type involving s.
5. The program must type check correctly when each pattern of type s is
treated as a pattern of type t. Within expressions, type s is considered
distinct from type t.
Notice that due to restrictions 3 and 5, a view function can construct a
value of type s, but cannot do anything with the value other than return it
as a result. Rule 3 prohibits updates and selection while rule 5 makes it
impossible to use pattern matching to extract information from a value of
type s, since no pattern is considered to have type s.
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.
5.1.1 Export Lists (changes)
----- ------ -----
In item 2, change "data or newtype" to "data, newtype or view".
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.
________________________________________________________________________
ADDITIONAL DISCUSSION
---------- ----------
Equational Reasoning
---------- ---------
One of the major complications with Phil Wadler's original proposal for
view, which allowed transformations to and from view types, is that the two
transformations were not always inverses. For example, when C is a view
constructor, the equation
let C y = C x in y
did 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 t2
is 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 y
syntactically 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 + 1
we 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).
Views and Classes
----- --- -------
We can implement complex numbers, using a polar representation and a polar
view, with the following module. Notice that the "MkCmplx" constructor is
not exported, allowing a change of representation.
> 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 t1
would have been equivalent to
> r2 = r1
> t2 = t1
This 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 t1
instead of
> Pole r2 t2 = pole r1 t1
which 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)
Views and Recursion
----- --- ---------
The restrictions on views allow several forms of recursion, as illustrated
by the following examples.
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
Total vs Partial Views
----- -- ------- -----
The use of view patterns may be mixed with the use of non-view patterns.
For example, using the Last view from above, we can define a function final
by:
> final [] = error "final: not defined for []"
> final (Last x) = x
However, 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.
If Haskell 1.3a allows selective export of constructors, then using a dummy
constructor that is not exported for cases where pattern matching should
fail may be useful. (I can't remember whether we have reversed ourselves
an odd or even number of times on the question of selectively exporting
constructors and class member functions.)
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.)
Views and Guards
----- --- ------
While we do not necessarily endorse the following programming style, in
many cases views may provide a more readable alternative to guards.
Experience will be necessary to determine whether this is really useful or
just a silly abuse of a new tool.
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 = n
and
> 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) x
In 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.
Views and Constructor Classes
----- --- ----------- -------
Wadler, in his original paper, gives an example in which a join (tree)
representation of a list can be viewed as an ordinary list. Since we
cannot have a single list type that is both an algebraic datatype and a
viewtype, we instead define a constructor class, "OrderContainer", that
contains the type constructors "[]" and "JoinList" as instances.
> 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.
Further Reading
------- -------
[1] Burton, F. W. and Cameron, R. D., "Pattern matching with abstract data
types." Journal of Functional Programming, 3, 2 (April 1993), 117-190.
[2] Pedro, P. G., Pe\~{n}a, R. and N\'{u}\~{n}ez, 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.
