On 24/09/2013, at 9:58 AM, srean wrote:

> I have to rewire my brain to this view, my comfort zone is still that
> type is a set on which certain functions can act.

No rewiring is required, just add the constraint "I do not know
what is in the set".

If you want an axiomatic description of how to do this: throw
out the Axiom of Choice. That is the axiom of ZF set theory
that lets you pull a random element out of a set.

Saying you don't know what's in a set is abstracting it.
Its "just a set".

Just for your amusement, you can recover the elements you just threw
away!

Its actually very simple, if you have a terminal object 1 in your
category, then every function:

        f: 1 -> T

picks out a particular element of T. In set theory a set with one element is 
terminal.

In Felix, there is a  terminal type written 

        unit = 1

which has exactly one value, the empty tuple

        ()

Note there are a lot of other terminals.

And now:

        fun one() => 1;
        fun two() => 2;
        ...

In fact you can see there is 1-1 correspondence between functions

        1-> int

and the members of your set int.

So .. your set is abstract .. you have no known values in it .. but you know
what the values are anyhow!

What is the point of all this?

In category theory you cannot APPLY a function to a value, because there
are no values.

But you can COMPOSE functions. So the application

        square 2

is not allowed. But you can instead do:

        compose (square, two)

and lo and behold this function is four.


--
john skaller
skal...@users.sourceforge.net
http://felix-lang.org




------------------------------------------------------------------------------
October Webinars: Code for Performance
Free Intel webinars can help you accelerate application performance.
Explore tips for MPI, OpenMP, advanced profiling, and more. Get the most from 
the latest Intel processors and coprocessors. See abstracts and register >
http://pubads.g.doubleclick.net/gampad/clk?id=60133471&iu=/4140/ostg.clktrk
_______________________________________________
Felix-language mailing list
Felix-language@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/felix-language

Reply via email to