Functional programming and William Lawvere's notion of "variable sets"(vs topos of "static sets") in a Topos ...

Functional programming and William Lawvere's notion of "variable sets"(vs topos of "static sets") in a Topos ...

[Vasili I. Galchin]

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/ ]

Re: Functional programming and William Lawvere's notion of "variable sets"(vs topos of "static sets") in a Topos ...

[Harley Eades III]

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/ ]