constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
internalization and categorical algebra
algebra object (associative, Lie, …)
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
In purely functional programming languages (such as Haskell) all would-be side effects are data typed in terms of monads in computer science which make the side effects look like and hence be formally treated like verifiable deterministic pure functions. If the actual side effect operations of reading input from or writing output to actual physical devices is typed in this monadic way, one speaks of an I/O-monad.
So to the programming language an IO-monad looks just like a state monad or similar, but when run on an actual computer the bind operation does cause actual physical effects.
Original discussion:
Review and exposition:
Nick Benton, John Hughes, Eugenio Moggi, §5.1 in: Monads and Effects, in: Applied Semantics, Lecture Notes in Computer Science 2395, Springer (2002) 42-122 [doi:10.1007/3-540-45699-6_2]
Bartosz Milewski, §21.2.8 & §21.29 in: Category Theory for Programmers, Blurb (2019) [pdf, github, webpage, ISBN:9780464243878]
In Haskell:
A Gentle Introduction to Haskell, Section 7: Input/Output
Wikipedia, IO monad (Haskell)
(…)
Last revised on August 28, 2023 at 16:07:43. See the history of this page for a list of all contributions to it.