Path: utzoo!censor!geac!torsqnt!news-server.csri.toronto.edu!cs.utexas.edu!uunet!mcsun!unido!fauern!opal!wg
From: wg@opal.cs.tu-berlin.de (Wolfgang Grieskamp)
Newsgroups: comp.lang.functional
Subject: Views revisited
Message-ID: <2634@opal.cs.tu-berlin.de>
Date: 13 Feb 91 23:13:52 GMT
Sender: news@opal.cs.tu-berlin.de
Reply-To: wg@opal.cs.tu-berlin.de
Followup-To: comp.lang.functional
Distribution: comp
Organization: Technical University of Berlin
Lines: 103
Nntp-Posting-Host: troll.cs.tu-berlin.de


A time ago there was a discussion about pattern matching in this 
newsgroup.  Some claimed arguments against pattern matching: 
A clean data type implementation should abstract from 
representation details to support locality of changes in a software 
system. Unfortunately, this contradicts to the kind of pattern matching
used in languages like ML, MIRANDA & HOPE, which requires global knowledge 
of data layout. But others argued, that most functional language users would 
not like to dispense with pattern matching since it supports a nice style 
of algorithm design closely related to structural induction. 

The model of *views* promises to integrate data abstraction and pattern 
matching: a view is an abstract sum-of-products interface to data types.
As people pointed out, views had been under discussion for the language
Haskell - but havent been took up in in the final language design.

Are views dead now? Does anyone knows about recent publications or
would like to comment on the following sketch out?


OPERATIONAL SEMANTICS OF VIEWS
==============================

Regarding to their operational semantics (and implementation), views are 
quite simple. Consider for example a view on natural numbers as a 
peano algebra:

	dataview nat = succ of nat | zero

Of course, natural numbers are not implemented this way, but the above
*view* may be implemented with abstract user functions:

	(* constructors *)
	val zero:nat
	fun succ:nat->nat
	(* discriminators *)
	fun is_zero:nat->bool
	fun is_succ:nat->bool
	(* selectors *)
	fun sel_succ:nat->nat

Pattern matching may now be purely source-transformed, for example:

	fun expon(x,zero) = 1
	  | expon(x,succ(y)) = x * expon(x,y)
	----------------V--------------------
	fun expon(x,y) = if is_zero(y) then 1
			 else if is_succ(y) then x*expon(x,sel_succ(y))
			      else "pattern exception"

This works fine for any view construction. Several pragmatic questions 
are pending:

-	should it be allowed to have several views on the same data type? 
-	if so, should it be allowed to mix views in one function definition? 
-	are views conciliatory with "best-fit" pattern matching? 


ALGEBRAIC SEMANTICS OF VIEWS
============================

Beside easy implementation, what is the *abstract* meaning of views?

(a)	should they satisfy reachability?
(b)	should they be considered as freely generating? 
(c)	should they be at least strongly normalizing?
(d)	should they relax reconstructability?

To explain, let v be a view on type t with constructors ci:ti->t, 
corrosponding selectors si:t->ti and discriminators di:t->bool. 

Now, with (a) one will have:

	FA x IN t . EX i . EX y IN ti . ci(y)=x	

(b) induces the usual laws on datatypes:

	FA i . FA x IN ti . si(ci(x)) = x		(b1)
	FA i . FA x IN ti . di(ci(x)) 			(b2)
	FA i . FA y IN t  . di(y) => ci(si(y)) = y	(b3)

With (c) free generating is restricted by congruence classes, but
there is a normal form:

	(b)-(b1,b2)
	+ FA i . FA y IN t . di(y) => si(ci(si(y)))=si(y)

With (d) there is some information "hidden" inside values which cannot 
be reconstructed:

	(b)-(b3) or
	(c)-(b3)



The current state of decision for the language OPAL here at the TUB 
is very conservative: views must be free generating and satisfy
reachability. 


--
Wolfgang Grieskamp 
wg@opal.cs.tu-berlin.de tub!tubopal!wg wg%opal@DB0TUI11.BITNET