Category theory for programmer notes
Posted on March 1, 2020
Tags: typetheory
1 Function composition
template<typename G, typename F>
auto compose(G&& g, F&& f) {
return [g,f](auto&& t) { return g(f(std::forward<decltype(t)>(t))); }; }
auto const id = [](auto&& t) -> decltype(t)&& { return std::forward<decltype(t)>(t); };
// Usage sample
auto const f = [](int v) { return v - 1.f; };
auto const g = [](float v) { return static_cast<int>(v); };
auto const g_after_f = compose(g ,f);
2 Top Type
- Top is called
void
in C++ butvoid
in haskell is Bottom or False. - Top aka True is constructed by one constant term true.
- term true proves the Type True
\[ \cfrac{}{}\]
template<class T>
void unit(T) {}
f44 :: () -> Integer
= 44 f44 ()
3 Bottom Type
- Bottom aka False has no constructor
- no term can construct Type False therefore there is no way to prove False
- Haskell bottom is called
void
. REMEMBERvoid
is not bottom in C++.
4 polymorphic types are Natural transformations
4.1 Either Sum Type
data Either Bool Int = Left Bool | Right Int
to :: Either Bool Int -> String
=
to x
from :: String -> Either Bool Int
"True" = Left True
from = Right 0
from _