On Thu, 2006-08-31 at 22:12 -0400, Peter Tanski wrote:
> On Aug 31, 2006, at 8:30 PM, skaller wrote:
> > There are a LOT of these operators. I plan to add them all,
> > but before I do I need to list them and try to figure a systematic
> > notation.
>
> I will try to help, if you want. Of course you know your creation best.
A list of categorical combinators requires knowing
some universal algebra .. not Felix.
I want Felix to model category theory as is possible,
since I have faith in it to deliver good stuff:
it is, after all, the mathematics of the extremely trival
designed for pedants and programmers.
I have a book with some common constructions in it,
but there are a lot of them, and programmers need a
different set to that required by mathematicians,
even category theorists: there won't be
a special notation for something not used a lot,
but programmer use things frequently that mathematicians
do not.
Composition, for all its merits, is rarely used in practice.
> > The HARD part is every such 'executable' expression has a
> > corresponding typing .. the type terms ALSO have to be
> > combined.
>
> Even after reading the rest of your message, I still don't understand
> the problem. The operator is executable, so it has the type:
>
> <,>:( a -> b) -> (c -> d) -> (b, d)
It's only a binary operator. Show me a definition that
works for n arguments .. without knowing n in advance.
For composition
a . b . c . d
works because composition is associative. But tuples are not.
So you don't have
<a,b,c> = <<a,b>,c>
but you DO have
a . b . c = (a.b).c = a.(b.c)
Remember most category theory, the theory of total pedantry,
actually says 'up to isomorphism' a lot. Tuple formation and
hence <..> operator isn't associative: that requires equality,
not just isomorphism.
> I think my confusion is with the type system. Following the tutorial
> example, no. 209:
>
> typedef fun pair (a:TYPE,b:TYPE):TYPE => a * b;
>
> a*b is a tuple type
int * long is the type of a pair of values.
TYPE * TYPE is the (meta)type of a pair of types.
[TYPE is the collection of all types]
1,2 is a pair of values
int,long is a pair of types
The bifunctor pair above is a mapping from the cartesian
product of the TYPE category with itself, to the TYPE category.
The product
TYPE * TYPE
is not the same category as
TYPE
any more than
int * int
is the same type as
int
This definition:
typedef fun pair (a:TYPE,b:TYPE):TYPE => a * b;
defines a function of kind
TYPE * TYPE -> TYPE
which takes a pair of types, and returns the corresponding
tuple type.
In other words, this (VERY IMPORTANT) function maps two
individual types to the corresponding tuple type.
The tuple type (int * long) is a SINGLE type,
it has a SINGLE value.
Another name for 'pair' is ',' except that the tuple
constructor isn't binary, but n-ary (chainable).
The reason this function is VERY IMPORTANT is that
it is the exception to the rule that functions only
have one argument. Most functions have kind:
TYPE -> TYPE
but the tuple constructor alone has kind:
TYPE * TYPE .... TYPE -> TYPE
This is precisely what allows multiple argument functions
to be treated uniformly by giving them a tuple argument,
but there has to be some way to make these tuples,
and that function has to accept multiple arguments.
The 'fun' thing is, of course, that the tuple constructors
own kind's domain is a single metatype:
TYPE * TYPE * .. * TYPE
of kind
METATYPE
so we can always reduce things to a uniform state by
going high enough up in the kinding system :)
--
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
