Draft:Functorial programming
Submission declined on 3 April 2024 by Vanderwaalforces (talk). This submission is not adequately supported by reliable sources. Reliable sources are required so that information can be verified. If you need help with referencing, please see Referencing for beginners and Citing sources.
Where to get help
How to improve a draft
You can also browse Wikipedia:Featured articles and Wikipedia:Good articles to find examples of Wikipedia's best writing on topics similar to your proposed article. Improving your odds of a speedy review To improve your odds of a faster review, tag your draft with relevant WikiProject tags using the button below. This will let reviewers know a new draft has been submitted in their area of interest. For instance, if you wrote about a female astronomer, you would want to add the Biography, Astronomy, and Women scientists tags. Editor resources
| ![]() |
Comment: Kindly see WP:INLINECITE and cite your sources, this is more or less an WP:OR if you do not cite your sources. Vanderwaalforces (talk) 21:57, 3 April 2024 (UTC)
Comment: I reverted my decline as existing as I misreading "Functorial programming" as "Functional programming". Noting here to make sure no one else makes that mistake KylieTastic (talk) 16:19, 3 April 2024 (UTC)
Functorial Programming is a programming paradigm derived from category theory, it is a theoretical framework in computer science and mathematical logic that extends classical type theory by introducing notions of directionality and computation flow into types. Although not originally termed as such, the foundational concepts of Functorial Programming can be traced back to Kosta Došen's seminal work, Cut-elimination in Categories (1999), which explored the intersections of category theory, logic, and computation, particularly through the lenses of cut-elimination.
Background
[edit]The concept of type theory has its roots in the work of Bertrand Russell and Alonzo Church, serving as a foundation for formal logic and computer science. However, traditional type theories often focus on the logical consistency and structure of mathematical statements without explicitly accounting for the computational processes or transformations between types. Functorial Programming aims to fill this gap by incorporating directional aspects into type relationships, drawing inspiration from category theory and the principles outlined in Došen's work.
Origins
[edit]Kosta Došen's Cut-elimination in Categories introduced the idea of cut-elimination from a categorical perspective, proposing a framework where logical deductions and computational processes could be represented as morphisms in a category. This approach laid the groundwork for thinking about types and computations in a directed manner, leading to the conceptualization of Functorial Programming.
Foundational Concepts
[edit]Functorial Programming builds upon several key concepts introduced by Došen:
- Cut-elimination: The process of simplifying logical proofs by eliminating intermediate steps or 'cuts,' reinterpreted in the context of category theory as the simplification of morphism compositions.
- Categories and Morphisms: Utilizes the language of category theory to formalize types as objects within a category and computations or transformations as morphisms between these objects.
- Substructural Logics: A class of logics that Dosen's work aligns with, characterized by their relaxation of structural rules, such as contraction and weakening, which are foundational in classical logic.
- Yoneda Lemma: A principle in category theory that relates functors to sets of natural transformations, instrumental in Dosen's formulation of Functorial Programming.
Development
[edit]Following the publication of Došen's book, researchers in the fields of computer science and logic began to explore the implications of his work for type theory and programming languages. This exploration led to the formal development of Functorial Programming, which explicitly integrates directionality into type relations and computations, offering a new perspective on type systems and functional programming.
Applications
[edit]Functorial Programming has potential applications in several areas of computer science, including:
- Functional Programming: Providing a more robust theoretical foundation for designing and reasoning about functional programs, especially in terms of composability and modularity.
- Concurrent and Distributed Systems: Modeling and verifying properties of concurrent and distributed systems, where the directionality of computation plays a crucial role.
- Proof Assistants and Automated Theorem Proving: Enhancing the capabilities of proof assistants and automated theorem provers by leveraging directed types
See also
[edit]Further reading
[edit]- Lambek, J., & Scott, P. J. Introduction to Higher Order Categorical Logic. Cambridge University Press, 1986.
- Pierce, Benjamin C. Types and Programming Languages. MIT Press, 2002.
References
[edit]- Došen, Kosta. Cut-elimination in Categories. Kluwer Academic Publishers, 1999.
Category:Type theory Category:Computer science Category:Mathematical logic Category:Category theory