Index: doc/proposals/exceptions-pab.md
===================================================================
--- doc/proposals/exceptions-pab.md	(revision cea0d0c1f38dd62a244e585e64531b78242825f3)
+++ doc/proposals/exceptions-pab.md	(revision 30901eb65d3c152c47452edacf66205ebf78996e)
@@ -59,5 +59,6 @@
 
 ```
-exception int dual( int, double ) dual;		// Dual, return result or exit handler block, no initial stack unwinding
+exception int dual( int, double ) dual;		// Dual, return result or exit handler block,
+											// no initial stack unwinding
 ```
 
@@ -66,8 +67,8 @@
 
 ```
-	} catch( int fix( int i, float j ) ) {	// stack not unwound, i and j accessible, must return
-		return 42;							// implies return to fix call, not return of nested function
+	} catch( int fix( int i, float j ) ) {	// stack not unwound, i/j accessible, => must return
+		return 42;							// => return to fix call, not return of lexical function
 		break;								// syntax error => must return
-		// fallthrough => syntax error
+		// fallthrough => must return
 	}
 ```
@@ -78,7 +79,7 @@
 ```
 	} catch( void recover( int i ) ) {		// stack unwound, cannot return
-		break;								// implies exit catch routine
-		return;								// implies return from lexical function
-		// fallthrough => implies break
+		break;								// => exit catch routine
+		return;								// => return from lexical function
+		// fallthrough => => break
 	}
 ```
@@ -88,7 +89,7 @@
 ```
 	} catch( int dual( int i, float j ) ) {	// stack not unwound, can return
-		return 42;							// implies return to fix call, not return of nested function
-		break;								// implies exit catch body
-		// fallthrough => implies break
+		return 42;							// => return to fix call, not return of nested function
+		break;								// => exit catch body
+		// fallthrough => break
 	}
 ```
@@ -96,67 +97,14 @@
 In all cases, a handler can raise another exception.
 
-An exception function can have a static body, which define the action if the exception is not caught.
-If no body is specified, there are default actions added.
-This matches with `defaultResume` and `defaultTerminate` in current C∀/μC++.
-Here a parameter name is necessary to access the raise argument(s).
-
-Resumption default:
-
-```
-exception int resumpt( int i ) {			// called if no handler found
-	// return default correction or abort or raise another exception
-	// default if not specified is to call UnhandledException at resumer or joiner.
-}
-```
-
-Termination default:
-
-```
-exception void termin( double d ) {			// called if no handler found
-	// abort or raise another exception
-	// default if not specified is to call UnhandledException at resumer or joiner.
-}
-```
-
-Dual default is the same as termination default, as having a default correction action is unlikely.
-
-A `throws` clause can be added to a regular function to indicate alternate outcomes.
-
-```
-int foo(...) throws( int ex( int ), float ex( int ), char ex( double, double ) );
-```
-
-The `throws` clause is *not* part of the function type, and hence, is not used for overloading.
-Functions with a `throws` clause cause are handled by a separate type-checking pass, which examines the statically call structure to determine if calls to `foo` are nested directly or indirectly within guarded blocks with matching catch clauses, e.g.:
-
-```
-int bar( int i ) throws( int fixup( int ) );
-
-void foo(...) {
-	... i = bar( 3 ); ...					// call statically nested within handler for fixup
-}
-void baz() {
-	try {
-		foo(...);
-	} catch( int fixup( int ) ) {
-		... return 42;
-	}
-}
-```
-
-If this type check fails, a warning is given, and a dynamic check is wrapped around the call to verify only the specified exception functions are raised.
-This dual approach allows all forms of reuse to exist, and is similar to checked/unchecked exceptions in Java.
-
 Resumption example:
 
 ```
-exception int fix( int i, float f );
-
+exception int fix( int, float );
 void foo() {
 	try {
 		for () {
-			if ( ... ) x = fix( 3, 5.4 );
+			... if ( ... ) x = fix( 3, 5.4 ); ...
 		}
-	} catch( int fix( int i, float j ) ) {
+	} catch( int fix( int i, float f ) ) {
 		... return 42;						// fix up problem and return to raise
 	}
@@ -168,10 +116,9 @@
 ```
 exception void end_of_file( ifstream is );
-
 void foo() {
 	int i;
 	try {
 		for () {
-			sin | i;  // internally, does a call end_of_file( is ), which implicitly throws exception
+			sin | i;			// internally, calls end_of_file( is ) to raise exception
 			sout | i;
 		}
@@ -185,6 +132,5 @@
 
 ```
-exception int dual( int i, float f ) dual;
-
+exception int dual( int i, float ) dual;
 void baz() {
 	try {
@@ -192,18 +138,186 @@
 			if ( ... ) x = dual( 3, 5.4 );
 		}
-	} catch( int dual( int i, float j ) ) {
+	} catch( int dual( int i, float f ) ) {	// stack not unwound
 		if ( ... ) return 42;				// return to raise calls
 		if ( ... ) break;					// exit catch body
-		// fallthrough						// implies break
-	}
-}
-```
-
-I'm not sure this polymorphism is doing anything, except suggesting a common pattern.
-A catch clause cannot be polymorphic because there is no RTTI matching.
-
-```
-forall( T ) exception void arithmetic( T op1, T op2, int retcode ) noreturn;
-
+		// fallthrough => break
+	}
+}
+```
+
+
+## Default Handler
+
+An exception function can have a static body, which defines the action if the exception is not caught.
+If no body is specified, there are default actions added.
+This matches with `defaultResume` and `defaultTerminate` in current C∀/μC++.
+Here a parameter name is necessary to access the raise argument(s).
+
+Resumption default:
+
+```
+exception int resumpt( int i ) {			// called if no handler found
+	// return default correction or abort or raise another exception
+	// default if not specified is to call UnhandledException at resumer or joiner.
+}
+```
+
+Termination default:
+
+```
+exception void termin( double d ) {			// called if no handler found
+	// abort or raise another exception
+	// default if not specified is to call UnhandledException at resumer or joiner.
+}
+```
+
+Dual default is the same as termination default, as having a default correction action is unlikely.
+
+
+## Polymorphism
+
+A catch clause can be polymorphic using the RTTI information in a mangled name.
+
+```
+forall( T | { T ?+?( T, T ); } )
+exception T foo( T t ) { return t + t; }
+
+	try (
+		i = foo( 3 );						// raise
+	} catch( int foo( int t ) ) {			// monomorphic handler
+		return t + 3 / t;					// can do something
+	} catch( forall( T | { T ?+?( T, T ) } ) T foo( T t ) ) { // polymorphic handler
+		return t + t;						// cannot do much
+	}
+
+```
+
+Matching is a pattern match on the mangled name (assuming there is enough information):
+
+```
+_X3fooQ1_0_0_5__X16_operator_assignFBD0_BD0BD0__X12_constructorFv_BD0__X12_constructorFv_BD0BD0
+	__X11_destructorFv_BD0__X13_operator_addFBD0_BD0BD0__FBD0_BD0__1
+```
+
+
+## Separate Compilation
+
+**test.hfa**
+
+```
+typedef struct S {
+	void (*f)( int );						// general function pointer
+} S;
+
+void foo( int ) throws( E );				// external
+void bar( int ) throws( F );
+
+void mary( S & s );							// external
+void jane( S s );
+```
+
+**test2.cfa**
+
+```
+#include "test1.hfa"
+#include "stdlib.h"
+
+void foo( int ) { printf( "foo\n" ); }
+void bar( int ) { printf( "bar\n" ); }
+
+void mary( S & s ) {
+	s.f = random() % 2 ? foo : bar;			// randomly insert a function
+}
+
+void jane( S s ) {
+	s.f( 3 );								// call field f
+}
+```
+
+**test1.cfa**
+
+```
+#include "test1.hfa"
+
+int main() {
+	S sfoo;
+
+	mary( sfoo );							// initialize field f
+
+	try {
+		jane( sfoo );						// calls sfoo.f in jane
+	} catch( ... ) {}						// cannot statically check correct handler is present
+}
+```
+
+
+## `throws` Clause
+
+A `throws` clause can be added to a regular function to indicate alternate outcomes.
+
+```
+int foo(...) throws( int ex( int ), float ex( int ), char ex( double, double ) );
+```
+
+The `throws` clause is *not* part of the function type, and hence, is *not* used for overloading.
+Functions with a `throws` clause are handled by a separate type-checking pass, which examines the static call-structure to determine if calls are nested directly or indirectly within guarded blocks with matching catch clauses, e.g.:
+
+```
+int bar( int i ) throws( int fixup( int ) ); // might call fixup directly or indirectly
+
+void foo(...) {
+	... i = bar( 3 ); ...			// call statically nested within handler for fixup in baz
+}
+void baz() {
+	try {
+		foo(...);
+	} catch( int fixup( int ) ) {			// handler for bar
+		... return 42;
+	}
+}
+```
+
+If this type check fails because of separate compilation, e.g., `baz` is in a different translation unit, a warning is given, and a dynamic check is wrapped around the call to `bar` to verify only the specified exception functions are raised.
+This dual approach allows all forms of reuse to exist, and is similar to checked/unchecked exceptions in Java.
+
+
+## Polymorphism Extension
+
+A new kind of polymorphic parameter is introduced, `throws`, listing the possible empty set of exceptions (alternate outcomes) that can be raised exception, but a possibly empty set of exceptions.
+A set of exceptions can be used in an exception signature in the same way a single exception can be and are traced from callee to caller in the same way a single exception is.
+They do not interact with throws or catches as those work on concrete types.
+At the top and bottom of the polymorphic call stack concrete functions throw and catch the exception, passing through the polymorphic section. 
+
+```
+forall( T, [N], throws E )
+	void apply( void op(T &) throws(E), array(T, N) & data ) throws(E) {
+		for ( i; N ) op( data[i] );
+}
+```
+Given the concrete usage:
+
+```
+void op( int ) throws( void WWW( int ), Y, Z ) { ... }
+array( int, 10 ) arr;
+try {
+	 apply( op, arr ); // op(... ) => if (... ) WWW(...)
+} catch( void WWW( int ) ) { ... // apply can raise from op
+} catch( exception Y ) { ... // apply can raise from op
+} catch( exception Z ) { ... // apply can raise from op
+}
+```
+
+The call to `apply` composes a list of all potential exceptions thrown by arguments.
+
+Imagine we passed around a set description (a list of type identities for each exception in the set) and at the edges of the polymorphic space we check for an unknown exception type against these sets.
+The static checks should ensure that every exception falls into one set;
+in fact if there is only one knows set we know it must belong to it.
+Then we wrap it up with a little marker saying which set it is part of and which one in the set it is.
+That gets passed through as an opaque exception until we return to monomorphic code, then it is unpacked and passed normally.
+
+
+## More Examples
+
+```
 enum FloatExceptions ! { Invalid, ZeroDiv, Overflow, Underflow, Inexact };
 exception double arithmetic( double op1, double op2, int retcode ) {
@@ -215,10 +329,10 @@
 }
 
-void xxx() {
+void foo() {
 	double x = 3.5;
 	try {
 		x = x / 0.0;
-	} catch( arithmetic( double op1, double op2, int retcode ) ) {
-		if ( retcode == FloatExceptions.ZeroDiv ) ...
+	} catch( double arithmetic( double op1, double op2, int retcode ) ) {
+		if ( retcode == FloatExceptions.ZeroDiv ) ...	// analyze retcode
 	}
 
@@ -226,7 +340,7 @@
 	try {
 		i = i / 0;
-	} catch( arithmetic( int op1, int op2, int retcode ) ) {
-		if ( retcode == IntExceptions.ZeroDiv ) ...
-	}
-}
-```
+	} catch( double arithmetic( int op1, int op2, int retcode ) ) {
+		if ( retcode == IntExceptions.ZeroDiv ) ...		// analyze retcode
+	}
+}
+```