Partial evaluations are a way to encode, in terms of monads, operations which have been computed only partially. For example, the sum "1+2+3+4" can be evaluated to "10", but also partially evaluated to "3+7", or to "6+4".
Such structures can be defined for arbitrary algebras over arbitrary monads, and even 2-monads, and can be considered the 1-skeleton of a simplicial object called the bar construction. The higher simplices of the bar construction can be interpreted as ways to compose partial evaluations. Recent research has shown that, while for cartesian monads partial evaluations form a category, for weakly cartesian monads the compositional structure is more complex, and in particular it does not in general form any of the standard higher-categorical structures.
Moreover, partial evaluations return known concepts of "partially evaluated operations" in the following contexts:
- For probability monads, where the operation is taking the expected value, partial evaluations correspond to conditional expectations;
- For the free cocompletion monad, where the operation is taking the colimit, partial evaluations correspond to left Kan extensions.Relevant papers:
- T. Fritz and P. Perrone, "Monads, partial evaluations and rewriting", arXiv:1810.06037;
- C. Constantin, T. Fritz, P. Perrone and B. Shapiro, "Partial evaluations and the compositional structure of the bar construction", arXiv:2009.07302;
- P. Perrone and W. Tholen, "Kan extensions are partial colimits", arXiv:2101.04531.
|
