On Sat, 2006-09-02 at 19:58 -0400, Peter Tanski wrote:
> On Sep 2, 2006, at 2:01 PM, skaller wrote:
> My personal head-banging came when trying to understand why the Felix
> function 'pair' created a unified TYPE rather than a product: TYPE *
> TYPE. After reading Cardelli's paper, I now understand that pair and
> tuple are (or should be) distinct types: pair is the product type,
> logically "AND," while tuple is the disjoint union type, logically "OR."
I don't really understand that either :)
The type function:
typedef fun pair (a:TYPE, b:TYPE):TYPE=> a * b;
takes two types as an argument, and returns a single type.
Since pair operator on types, its type is sometimes
called its kind to avoid confusion:
TYPE * TYPE -> TYPE
This function is an arrow in the meta-category consisting
of categories TYPE, and all finite products and functors
between them.
I write the inverse, which is a partial function:
typedef fun unpair(a: TYPE): TYPE * TYPE =>
typematch a with
| ?a * ? b => a,b
endmatch
;
So there is an isomorphism between the product category
TYPE * TYPE
and the subcategory of TYPE with elements
PAIRS = { x in TYPE | x = a * b }
and all arrows between them.
The whole of the above can be repeated for sums and also
the exponential ->
For example there is a map:
cases: TYPE * TYPE -> TYPE
(int, long) |-> int + long
This is less confusing: the kind of the LHS is still a product
of categories, but the RHS is not a product type but a sum type.
Smly:
exp: TYPE * TYPE -> TYPE
(int, long) |-> int -> long
--
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
