Functional programming and William Lawvere's notion of "variable sets"(vs topos of "static sets") in a Topos ...
Dear Cat People ... I have been re-reading William Lawvere's description of "variable sets" (a functor category) in "a elementary topoi" on a discrete poset/preset vs a "abstract sets" in the topos of abstract sets . In Haskell( and other FPLs .. ) aren't "pure" computations just over the topos of abstract sets and "mutable" /"time-varying/stateful" computations aren't just "variable sets" (i.e. a functor over a discrete preset-poset)?? Please forgive my germ of an idea Kind regards, Vasya P.S. Yes I am familiar with Eugenio Moggi's papers on using monads for stateful computations .. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Hi, Vasya. Something you might find interesting is that stateful computations can be modeled — very nicely in fact — using co-algebras. They have been used to give a formal semantics to object oriented (OO) programming languages, as well, as embedding OO in purely functions programming languages. I am not aware of a connection between co-algebras and variable sets, but I am not familiar with the latter. I just thought you might find these interesting. Thanks, .\ Harley Here are a list of references from my DB: @article{Setzer:2006, Author = {Anton Setzer}, Journal = {Trends in Functional Programming}, Title = {Object-Oriented Programming in Dependent Type Theory}, Year = {2006}} @article{Jacobs:2003, Author = {Bart Jacobs and Erik Poll}, Journal = {Theoretical Computer Science}, Number = {3}, Pages = {329 - 349}, Title = {Coalgebras and monads in the semantics of Java}, Volume = {291}, Year = {2003}} @article{Jacobs:2002b, Author = {Jacobs, Bart}, Journal = {Mathematical. Structures in Comp. Sci.}, Month = dec, Number = {6}, Pages = {875--903}, Title = {The Temporal Logic of Coalgebras via Galois Algebras}, Volume = {12}, Year = {2002}} @incollection{Jacobs:2002, Author = {Jacobs, Bart}, Booktitle = {Algebraic and Coalgebraic Methods in the Mathematics of Program Construction}, Editor = {Backhouse, Roland and Crole, Roy and Gibbons, Jeremy}, Pages = {237-281}, Publisher = {Springer Berlin Heidelberg}, Series = {Lecture Notes in Computer Science}, Title = {Exercises in Coalgebraic Specification}, Volume = {2297}, Year = {2002}} @article{Jacobs:2002a, Author = {Bart Jacobs}, Journal = {Electronic Notes in Theoretical Computer Science}, Number = {1}, Pages = {112 - 134}, Title = {Comprehension for Coalgebras}, Volume = {65}, Year = {2002}} @article{Rothe:2001, Author = {Jan Rothe and Hendrik Tews and Bart Jacobs}, Journal = j-jucs, Month = {feb}, Number = {2}, Pages = {175--193}, Title = {The Coalgebraic Class Specification Language CCSL}, Volume = {7}, Year = {2001}} @article{Kurz:20011, Author = {Alexander Kurz}, Journal = {Theoretical Computer Science}, Number = {1--2}, Pages = {119 - 138}, Title = {Specifying coalgebras with modal logic}, Volume = {260}, Year = {2001}} @article{Jacobs:2000, Author = {Bart Jacobs}, Journal = {Electronic Notes in Theoretical Computer Science}, Number = {0}, Pages = {160 - 195}, Title = {Towards a Duality Result in Coalgebraic Modal Logic}, Volume = {33}, Year = {2000}} @article{Hensel:1999, Author = {Hensel, U and Jacobs, B}, Journal = {Journal of Logic and Computation}, Number = {4}, Pages = {463-500}, Title = {Coalgebraic theories of sequences in PVS}, Volume = {9}, Year = {1999}} @article{Jacobs:1999, Author = {Bart Jacobs}, Journal = {Newsletter 3 of the Dutch Association for Theoretical Computer Science (NVTI)}, Pages = {15-27}, Title = {Coalgebras in Specification and Verification for Object-Oriented Languages}, Year = {1999}} @article{Jacobs:1998a, Author = {Jacobs, Bart and van den Berg, Joachim and Huisman, Marieke and van Berkum, Martijn and Hensel, U. and Tews, H.}, Journal = {SIGPLAN Not.}, Month = oct, Number = {10}, Pages = {329--340}, Title = {Reasoning About Java Classes: Preliminary Report}, Volume = {33}, Year = {1998}} @incollection{Hensel:1998, Author = {Hensel, Ulrich and Huisman, Marieke and Jacobs, Bart and Tews, Hendrik}, Booktitle = {Programming Languages and Systems}, Editor = {Hankin, Chris}, Pages = {105-121}, Publisher = {Springer Berlin Heidelberg}, Series = {Lecture Notes in Computer Science}, Title = {Reasoning about classes in object-oriented languages: Logical models and tools}, Volume = {1381}, Year = {1998}} @article{Jacobs:1998, Author = {Bart Jacobs}, Journal = {Electronic Notes in Theoretical Computer Science}, Number = {0}, Pages = {231 - 242}, Title = {Coalgebraic Reasoning about Classes in Object-Oriented Languages}, Volume = {11}, Year = {1998}} @incollection{Jacobs:1996, Author = {Jacobs, Bart}, Booktitle = {Object Orientation with Parallelism and Persistence}, Editor = {Freitag, Burkhard and Jones, CliffB. and Lengauer, Christian and Schek, Hans-J{\"o}rg}, Pages = {83-103}, Publisher = {Springer US}, Series = {The Kluwer International Series in Engineering and Computer Science}, Title = {Objects And Classes, Co-Algebraically}, Volume = {370}, Year = {1996}} On Aug 4, 2014, at 3:03 AM, Vasili I. Galchin <vigalchin@gmail.com> wrote:
Dear Cat People ...
I have been re-reading William Lawvere's description of "variable sets" (a functor category) in "a elementary topoi" on a discrete poset/preset vs a "abstract sets" in the topos of abstract sets . In Haskell( and other FPLs .. ) aren't "pure" computations just over the topos of abstract sets and "mutable" /"time-varying/stateful" computations aren't just "variable sets" (i.e. a functor over a discrete preset-poset)?? Please forgive my germ of an idea
Kind regards,
Vasya
P.S. Yes I am familiar with Eugenio Moggi's papers on using monads for stateful computations ..
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
participants (2)
-
Harley Eades III -
Vasili I. Galchin