4 ms·
You don't need to go deep. Types and functions (ignoring non-termination) form a category. Functional programming (Haskell programmers in particular) uses many
by gclaramunt 12y ago
You don't need to go deep. Types and functions (ignoring non-termination) form a category. Functional programming (Haskell programmers in particular) uses many results from it.
e.g.
building any "container" type (collections, options, futures,etc..) is the mapping of objects of an (endo) functor, the mapping of functions is given by fmap/map
As an example, just from the functor laws you get map (f.g) = map f . map g
Natural transformations between functors gives you parametricity and "theorems for free"
Another result that's used directly is the CoYonneda lemma (but I'm still trying to understand it :) )
The point is: category theory in spite of being totally abstract offers many interesting results that can be applied to day-to-day coding :)
- ihm 12y ago> Natural transformations between functors gives you parametricity and "theorems for free" Could you elaborate? This is something everyone always talks about but I've never really seen a proof/precise statement.
- gclaramunt 12y agoThe "Theorems for free" paper is here: http://ttic.uchicago.edu/~dreyer/course/papers/wadler.pdf http://ttic.uchicago.edu/~dreyer/course/papers/wadler.pdf ( I guess is the most precise you can get :) )
- tome 12y ago> Types and functions (ignoring non-termination) form a category Even including non-termination they form a category.
- gclaramunt 12y agoTrue, if I recall correctly, having bottom everywhere just complicates things without adding much value.
- tel 12y agoIt just means that you have a category where the objects are CPOs instead of sets or types or whatever. It can actually add a whole lot of value to describing the laziness story.
- gclaramunt 12y agoTrue, I actually was thinking about a Cartesian Closed Category (as explained in https://www.haskell.org/haskellwiki/Hask https://www.haskell.org/haskellwiki/Hask )