Categorical ML — Category-theoretic modular programming |
| |
Authors: | Esther Dennis-Jones Dr David E Rydeheard |
| |
Affiliation: | (1) Department of Computer Science, The University, Oxford Road, M13 9PL Manchester, UK |
| |
Abstract: | We consider an extension of the functional programming language Standard ML with a modular structure based upon concepts in category theory such as categories, functors, natural transformations and adjunctions. In essence, we are following the categorical imperative of considering arrows as well as objects. This is intended to enforce a certain mathematical rigour on the programmer, so that the only programs that can be expressed are those with a categorical significance. The essentially algebraic nature of category theory means that we may generate equational correctness conditions for the modular structure of programs, thus separating the correctness of individual functions from that of modules. We describe this programming language, give examples of its use, and explain how it is implemented in a type system. |
| |
Keywords: | Program modules Category theory Functional programming |
本文献已被 SpringerLink 等数据库收录! |
|