/sci/ - Science & Math

>>8097159
(cont.)

Of, in category, you have the famous Yoneda lemma which says that
Hom(Hom(A,-),F-)
is in bijection with
FA
where F is a functor, Hom(A,-) is the functor mappying object B to the function space B^A and the outer Hom gives a functions space between functors, meaning a set of natural transformations, which is Haskell are polymorphic functions (functions that work for all types in the system, such as "the" identity function, existing for both strings and ints)

Now take e.g. F to be the functor mapping types A to lists of terms of type A,
e.g. integers -4, 6, 25,... to lists of such integers, e.g. [3,-4,6], [-4], [8,26],...

The claim now is that for any type B, there is a bijection that takes a term of FA, i.e. some list k of A terms, to a term of
Hom(Hom(A,B),FB)
i.e. a map that takes a functions u in B^A to a term of lists of B's.

Let e.g. be A integers and B strings, so that a function in B^A would be, as an exmaple, the map from the number 3 to the word "three".
Now indeed, if k is fixed a list of integers (say [3,-4,6]), then you can define the function that takes any -any- function u from integers to strings and maps it to the list obtained by applying u to each of the entries in in k.
That is to say, the term [3,-4,6] corresponds to 'the function that takes any function u and returns the list [u(3), u(-4), u(6)]'.
But the point is that you can code this all up, and polymophically, i.e. indenpendent of any particular type like the integers.

The point that I want to make is that category theory cleans up your type system by pointing out all the natural maps, everything that obeys algebraic laws (I mean category theory was literally invented in the 40's to define the polymorphic functions / functions that work for a whole category / natural transformations).

Sure, you can learn haskell and understand what the Yoneda lemma isomorphism is doing without knowing that it's a concept found and used first by homologists etc. in the 40's.