Category Theory

The Axiom of Choice can be expressed as follows in Church's type theory:

(9^α) ∃x_α p_οαx_α ⊃ p_οα[ι_α(οα) p_οα]

Chomsky

Denotational Semantics

General Covariance

do -> dee -> doo -> zig zag -> chasing diagrams

Category Theory

A directed graph consists of a set of arrows and a set of vertices, and two functions from the arrow set to the vertex set, specifying each arrow's start and end vertex. The category of all directed graphs is thus nothing but the functor category Set^C, where C is the category with two objects connected by two morphisms, and Set denotes the category of sets.


Today I wrote this:

template < typename S, typename T >
class Attachment
{

public:
    Attachment( const S& src=S(), const T& tgt=T()) :

                        _src(src),_tgt(tgt) {}

    S src() const { return _src;}
    T tgt() const { return _tgt; }

    void set_src(const S& s) { _src = s;}
    void set_tgt(const T& t) { _tgt = t;}

private:
    S _src;
    T _tgt;

};

So... hmmm... I thought when I wrote that guy --- wow, a way to relate any class to any class.


But really, you know what?  First, I don't understand what those links point to.  I wish I understood.  I wish I could go back to school sometimes.  But if I did, I'll tell you what, I don't think I could write a program that will work.  I need to find the theorem that proves that I can't write good programs.

Vetter's Theorem: It's impossible to write a computer program that will make me understand how to program well.

And I'm thinking about whatever category theory is and how it relates to type theory and formal languages... and think I've been sniffing all around this... and it's eating at me.

There is just sooooo much knowledge out there... and programming remains completely and totally difficult.  I'm so frustrated with myself!  All the time!

What's cool is that I feel a strongly typed language pushing me towards solving something a certain way... and a lot of time it turns out to be better.  It's interesting how *language*, this static thing, when used will tailor the speaking of the solution.


I better sleep on it.

Day Four with no alcoholic beverage...

Hmmm.... Diagrammatic Reasoning - i so wish I could find some old math papers... I used to come up with a diagram for everything I solved... I remember having the most weird signs and symbols... and lines connecting junk.