Monad Computations in Type Theoretical Semantics
DOI:
https://doi.org/10.47850/RL.2023.4.4.70-81Keywords:
semantics, natural language, type theory, monads, computations, AgdaAbstract
Monad is a construction from the category theory, which could be understood as an abstraction
of computation [Moggi, 1991]. This is a computation resulting not simply in the computed value but in this value with
an additional structure. In recent years, monad in this sense has been successfully applied to natural language semantics in the
framework of Montague’s formalism. This article deals with monad computation applications in type theoretical semantics
[Ranta, 1994]. Several examples illustrate the usage of monads as well as applicative functors for contexts accounting
in various situations, controlling the order of quantifiers, belief reports formalization. The language of formalization is Agda
References
Agda Documentation (2023). Available at: https://agda.readthedocs.io/ (Accessed: 10 July 2023).
Asudeh, A. (2014). Monads: Some Linguistic Applications. Available at: http://www.sas.rochester.edu/lin/sites/asudeh/handouts/asudeh-se-lfg13.pdf (Accessed: 10 July 2023).
Asudeh, A. and Giorgolo, G. (2020). Enriched Meanings. Natural Language Semantics with Category Theory. Oxford. OUP. 179 p.
Barker, C. (2002). Continuations and the nature of quantification. Natural Language Semantics. Vol. 10. no. 3. pp. 211-242.
Barker, C. and Shan, C.-c. (2014). Continuations and Natural Language. Oxford. OUP. 230 p.
Luo, Z. (1994). Computation and Reasoning. A Type Theory for Computer Science. Oxford. OUP. 228 p.
Martin-Löf, P. (1984). An Intuitionistic Type Theory. Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980. Napoli. Bibliopolis. 91 p.
Moggi, E. (1991). Notions of computation and monads. Information and Computation. Vol. 93. no. 1. pp. 55-92. DOI: 10.1016/0890-5401(91)90052-4.
Montague, R. (1974). Formal Philosophy. Selected Papers of Richard Montague. Thomason, R. H. (ed.). With an intro. by Thomason, R. H. New Haven and London. Yale University Press. 369 p.
Norell, U. (2009). Dependently Typed Programming in Agda. In Koopman, P., Plasmeijer, R., and Swierstra, D. (eds.). Advanced Functional Programming: 6th International School, AFP 2008. Berlin, Heidelberg. Springer-Verlag. pp. 230-266. DOI: 10.1007/978-3-642-04652-0_5.
Ranta, A. (1994). Type-theoretical grammar. Clarendon Press. 226 p.
Wadler, P. L. (1994). Monads and composable continuations. Lisp and Symbolic Computation. Vol. 7. no. 1. pp. 39-56.
Downloads
Published
How to Cite
Issue
Section
License
This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.
https://oc.philosophy.nsc.ru/remote.php/webdav/%D0%94%D0%BE%D0%B3%D0%BE%D0%B2%D0%BE%D1%80%20%D1%81%20%D0%B0%D0%B2%D1%82%D0%BE%D1%80%D0%BE%D0%BC%20RL-%D0%BF%D1%80%D0%B0%D0%B2.doc
