I have added a new 'feature' to the Felix type system as shown
by the example here:
------------------------------
#include <flx.flxh>
typedef pairil = typecase [a] int+a => a * int endcase (int+long);
var x : pairil = 1L,2;
proc p(x: pairil) {
match x with
| ?a,?b => { print a; print ","; print b; endl; }
endmatch;
}
p x;
------------------------
.. debug stuff ..
1,2
-----------------------
As you may or may not know, Felix already supports some
interesting type system features. It purports to support
a typed lambda calculus whose primitives are base Felix
type terms, enriched by products, conditionals based
on unit sum types, and pattern matching.
The construction here:
typecase [a] int+a => a * int endcase
is a concrete representation of Barry Jays 'case' construction,
described in his paper on Pure Pattern Calculus.
The pattern calculus is a new calculus that subsumes lambda
calculus and supports many interesting kinds of polymorphism.
See:
http://www-staff.it.uts.edu.au/~cbj/patterns/
and download and read:
http://www-staff.it.uts.edu.au/~cbj/Publications/purepattern.pdf
The paper is very easy to read. The construction above is
is a (type) function, applied to a type like:
typecase [v1, v2, ..] pattern => result endcase argument
The pattern and result are ordinary types. The pattern must
contain exactly one occurence of each of the names v1, v2, ..
The semantics are to match the pattern against the argument
to obtain a binding for v1, v2, .. which when substituted
into the pattern yields the argument, and then substitute
those variables instead into the result.
This is very similar to the existing typematch facility:
typedef fun X(argument:TYPE):TYPE =>
typematch argument with
| pattern => result
endmatch
;
with one crucial difference (apart from being anonymous):
the typematch construction pattern has the variables
v1, v2, ... labelled inside the pattern, for example:
| ?U + ?V => U * V
but the Jcase construction is:
typecase [U,V] U + V => U * V endcase
and has the variables named separately. Although this seems
like a small difference, you will note that it allows
the pattern type itself to be an application of a Jcase
to an argument.
Contrast this with normal patterns, where the patterns
just consist of constants: Jpatterns are ordinary
terms, and thus can be *calculated*.
Interestingly, the Felix type unification engine has always
supported this construction implicitly: the base engine
already accepts a set of equations and a set of variables,
and has to solve the equations to find these variables.
It isn't possible to do a match with a unification
algorithm otherwise.
The addition of this feature to the type system may lead
to the elimination of the existing lambda forms, although
at present the lambda forms are typed by a kinding system
and support higher order entities, whereas my current
implementation of the pattern calculus ONLY supports types.
The notation is likely to replaced: in the paper Barry uses
the notation
pat --->_{vars} result
that is, the varset is a subscript of the arrow, and this
infix form seems much cleaner, so you can write
x --> y --> z
etc (with the subscripts on the arrows not shown here).
This is just a syntactic nit.
If the experiment goes OK, I may look at providing this
kind of matching for executable expressions.
--
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net
-------------------------------------------------------------------------
Using Tomcat but need to do more? Need to support web services, security?
Get stuff done quickly with pre-integrated technology to make your job easier
Download IBM WebSphere Application Server v.1.0.1 based on Apache Geronimo
http://sel.as-us.falkag.net/sel?cmd=lnk&kid=120709&bid=263057&dat=121642
_______________________________________________
Felix-language mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/felix-language
