"Applied functional type theory"
"Applied functional type theory" is a tentative name for the theory underlying modern functional programming.

All my technical posts on this topic so far:


2017-03-26 Functional programming and the real world https://chaource.dreamwidth.org/161590.html

2016-06-28 Functional programming is physics https://chaource.dreamwidth.org/143497.html

2016-08-30 Example of the use of category theory in functional programming https://chaource.dreamwidth.org/148979.html

2013-05-24 Lambda-calculus without recursion https://chaource.dreamwidth.org/93438.html

2015-04-09 Exercises in Curry-Howard correspondence https://chaource.dreamwidth.org/125399.html

2016-05-29 Polynomial functors I. Basic motivations. All polynomial type constructors are functors https://chaource.dreamwidth.org/140652.html

2016-06-01 Polynomial functors II. Basic definitions: (co)pointed, (co)distributive, (co)monadic. Monadic functors are distributive https://chaource.dreamwidth.org/140862.html

2016-06-02 Co-pointed functors are co-distributive https://chaource.dreamwidth.org/141143.html

2016-06-03 Polynomial functors III: all polynomial functors are (co)distributive https://chaource.dreamwidth.org/141503.html

2016-06-05 Polynomial functors IV: all polynomial functors are pre-(co)-monadic https://chaource.dreamwidth.org/141702.html

2016-06-10 Polynomial functors V: recursive functors are (co)distributive https://chaource.dreamwidth.org/141968.html

2016-06-16 Polynomial functors VI: An elementary question about polynomials, or How to characterize pairs of functors with natural transformations between them https://chaource.dreamwidth.org/142433.html

2016-06-22 Polynomial functors VII. Pointed and co-pointed recursive polynomial functors https://chaource.dreamwidth.org/143092.html

2016-06-30 Exponential-polynomial functors, contrafunctors, and profunctors https://chaource.dreamwidth.org/143705.html

2016-07-02 Exponential-polynomial profunctors II. Modularity with respect to a monoid https://chaource.dreamwidth.org/144118.html

2016-07-17 Tutorial on the free monad https://chaource.dreamwidth.org/144787.html

2016-07-19 Functors of functors. Deriving the "free monad". All recursive polynomial functors are pre-monadic https://chaource.dreamwidth.org/145119.html

2016-07-21 Polynomial functors VIII. Some recursive polynomial functors are pre-comonadic https://chaource.dreamwidth.org/145578.html

2016-07-22 Polynomial functors IX. Pre-monadic and pre-comonadic recursive functors https://chaource.dreamwidth.org/145721.html

2016-07-31 Representable functors and GADTs https://chaource.dreamwidth.org/146894.html

2016-08-04 Free functors, free applicatives, free monads I https://chaource.dreamwidth.org/147004.html

2016-08-07 Free functors, free applicatives, free monads II https://chaource.dreamwidth.org/147235.html

2016-08-09 Free functors, free applicatives, free monads III https://chaource.dreamwidth.org/147892.html

2016-08-11 Free functors, free applicatives, free monads IV https://chaource.dreamwidth.org/148057.html

2016-08-31 Initial F-algebras and free F-algebras over a type https://chaource.dreamwidth.org/149039.html

2016-10-04 The center-of-mass monad https://chaource.dreamwidth.org/150558.html


2017-03-05 All (recursive) polynomial functors are traversable https://chaource.dreamwidth.org/160254.html

2017-03-06 Monad transformers for exp-polynomial monads I https://chaource.dreamwidth.org/160492.html

2017-03-08 Monad transformers for exp-polynomial monads II https://chaource.dreamwidth.org/160598.html

2017-03-10 Exponential-polynomial applicative functors https://chaource.dreamwidth.org/160849.html

2017-03-13 Exponential-polynomial monads https://chaource.dreamwidth.org/161043.html

2017-03-19 Contrafunctors cannot be distributive or traversable https://chaource.dreamwidth.org/161356.html

2017-04-03 Monad transformers and free monads https://chaource.dreamwidth.org/161968.html

2017-04-15 Monads and monad transformers: The errors of my ways https://chaource.dreamwidth.org/162150.html