Comments on: Plain containers and linear logic… http://sneezy.cs.nott.ac.uk/containers/blog/?p=24 East Midlands Containers Ltd. Wed, 22 May 2013 16:51:41 +0000 http://wordpress.org/?v=2.5.1 By: Hank http://sneezy.cs.nott.ac.uk/containers/blog/?p=24#comment-21 Hank Mon, 12 Sep 2005 23:40:03 +0000 http://sneezy.cs.nott.ac.uk/containers/?p=24#comment-21 Concerning setoids, the "Container Gang" before the Coming of Hancock, have a paper Constructing Polymorphic Programs with Quotient Types from 2004 explaining the East Midlands take on quotienting the positions. (You probably have had a look.) Conor has some further ideas that must be somehow related about putting well-orders on positions, that are somewhere in this blog. They both seem to involve putting some structure on positions. I am very curious about the relations between containers with quotients and "species of structures" a la Fiore/Joyal/.. . Species seem very oriented towards data-structures with a finite number of distinguishable positions. Concerning setoids, the “Container Gang” before the Coming of Hancock, have a paper Constructing Polymorphic Programs with Quotient Types from 2004 explaining the East Midlands take on quotienting the positions. (You probably have had a look.)

Conor has some further ideas that must be somehow related about putting well-orders on positions, that are somewhere in this blog. They both seem
to involve putting some structure on positions.

I am very curious about the relations between containers with quotients and “species of structures” a la Fiore/Joyal/.. . Species seem very oriented towards data-structures with a finite number of distinguishable positions.

]]> By: PierreH http://sneezy.cs.nott.ac.uk/containers/blog/?p=24#comment-20 PierreH Mon, 05 Sep 2005 09:49:36 +0000 http://sneezy.cs.nott.ac.uk/containers/?p=24#comment-20 About multisets in type theory: the easiest is probably to use setoids and define [tex]\mathcal{M}(S,\equiv) := (\mathbf{List}(S),\approx)[/tex], where [tex]\approx[/tex] is just the "quotient" of [tex]\equiv[/tex] modulo permutations of lists. (Of course, we must require that the family of shapes is a family of setoids, indexed by a setoid: it must respect equality... This gets very messy...) Then, an action/shape is just given by a tuple [tex][s_1,\ldots,s_n][/tex], and a reaction/position is just a tuple of [tex][p_1,\ldots,p_n][/tex], where each [tex]p_i[/tex] is a position in shape [tex]s_i[/tex]. Note that this is not the same as the bang defined on interaction systems, since the number of actions/shapes is not determined by the state. In particular, while iterating the container, the number of shapes can change. That [tex]!C[/tex] is the free [tex]\otimes[/tex] comonoid just means that it is the "smallest" such comonoid: (1) there is an arrow [tex] e : !C \to \mathbf{Skip}[/tex] (2) there is an arrow [tex] !C \to !C \otimes !C[/tex] Those arrows satisfy some commutativity and associativity diagrams, and are universal in some sense ("free"). A more abstract way to look at it is by saying that the functor [tex]!\_[/tex] from the category of containers to the category of [tex]\otimes[/tex]-comonoids is adjoint to the obvious forgetful functor from [tex]\otimes[/tex]-comonoids to the containers... All of this seems very important to LL people, but I have to admit I don't have strong intuitions about them... About the link between container morphisms and simulations between interaction systems: the relation seems very subtle. When I wrote that container morphisms are all "equal" I had the "classical" notion of simulation: usual relations. In the case of containers, the set of states are trivial: [tex]\{*\}[/tex]. There is only one non-empty relation between two such sets: [tex]\{(*,*)\}[/tex]. In a constructive setting, this is far more complex than that! About multisets in type theory:

the easiest is probably to use setoids and define \mathcal{M}(S,\equiv) := (\mathbf{List}(S),\approx), where \approx is just the “quotient” of \equiv modulo permutations of lists.

(Of course, we must require that the family of shapes is a family of setoids, indexed by a setoid: it must respect equality… This gets very messy…)

Then, an action/shape is just given by a tuple [s_1,\ldots,s_n], and a reaction/position is just a tuple of [p_1,\ldots,p_n], where each p_i is a position in shape s_i.

Note that this is not the same as the bang defined on interaction systems, since the number of actions/shapes is not determined by the state. In particular, while iterating the container, the number of shapes can change.

That !C is the free \otimes comonoid just means that it is the “smallest” such comonoid:
(1) there is an arrow e : !C \to \mathbf{Skip}
(2) there is an arrow !C \to !C \otimes !C
Those arrows satisfy some commutativity and associativity diagrams, and are universal in some sense (”free”).

A more abstract way to look at it is by saying that the functor !\_ from the category of containers to the category of \otimes-comonoids is adjoint to the obvious forgetful functor from \otimes-comonoids to the containers…

All of this seems very important to LL people, but I have to admit I don’t have strong intuitions about them…

About the link between container morphisms and simulations between interaction systems: the relation seems very subtle. When I wrote that container morphisms are all “equal” I had the “classical” notion of simulation: usual relations. In the case of containers, the set of states are trivial: \{*\}. There is only one non-empty relation between two such sets: \{(*,*)\}.

In a constructive setting, this is far more complex than that!

]]> By: Hank http://sneezy.cs.nott.ac.uk/containers/blog/?p=24#comment-19 Hank Fri, 02 Sep 2005 05:08:36 +0000 http://sneezy.cs.nott.ac.uk/containers/?p=24#comment-19 I don't completely understand "all the container morphisms are equal when seen as interaction system morphisms". The relation between these two kinds of morphisms seems very subtle. It seems to me that a dependent container morphism (one with a *function* mapping high-level sorts to low-level sorts) is the same as an interaction system morphism which happens to be (the graph of) a total function. I can see, I think, that several different container morphisms can "satisfy" extensionally the same simulation relation, but not that all container morphisms are extensionally equal. I don’t completely understand “all the container morphisms are equal when seen as interaction system morphisms”. The relation between these two
kinds of morphisms seems very subtle. It seems to me that a dependent
container morphism (one with a *function* mapping high-level sorts to
low-level sorts) is the same as an interaction system morphism which happens to be (the graph of) a total function.

I can see, I think, that several different container morphisms can “satisfy” extensionally the same simulation relation, but not that all container morphisms are extensionally equal.

]]> By: Hank http://sneezy.cs.nott.ac.uk/containers/blog/?p=24#comment-17 Hank Thu, 01 Sep 2005 10:56:09 +0000 http://sneezy.cs.nott.ac.uk/containers/?p=24#comment-17 About representing multisets in type theory, one option seems to be as a quotient of [tex] $(\Sigma\,n : N) n \rightarrow S$ [/tex] (here the second "n" is being used for the set "Fin(b)" or [tex] $ \{ i : N \,|\, i S$ [/tex]. About Pierre's suggestion for a bang on plain containers, I take it the idea is that <blockquote> (1) an angel's move (shape) in the bang of a contrainer is a multiset of angel's moves (shapes) in the unbagged container [tex] $(C!).A = (C.A)!$[/tex]. We now have to arrange that the set of positions for a shape does not depend on the particular order in which a shape is given. (2) a demon's response (position) to an angel's move [tex] $a = [a_0,...,a_{n-1}]$ [/tex] is (represented by) a permutation p of dom(a), and a function [tex] $d : (\Pi i : dom(a)) \rightarrow (C.D)(a(p(i)))$ [/tex]. Equality of representations is modulo permutations. </blockquote> It is as iff the angel has an inexhaustible supply of slave devices to which she can issue as many commands in parallel as she likes (possibly none). But she has to wait for all the responses. What does one have to show about this? That C! is the free [tex]$\otimes$[/tex] comonoid generated by C? What is this in layman's terms? About representing multisets in type theory, one option
seems to be as a quotient of $(\Sigma\,n : N) n \rightarrow S$
(here the second “n” is being used for the set “Fin(b)” or
$ \{ i : N \,|\, i S$ .

About Pierre’s suggestion for a bang on plain containers, I take
it the idea is that

(1)

an angel’s move (shape) in the bang of a contrainer is a multiset of angel’s moves (shapes) in the unbagged container $(C!).A = (C.A)!$. We now have to arrange that the set of positions for a shape does not depend on the particular order in which a shape is given.

(2)

a demon’s response (position) to an angel’s move $a = [a_0,...,a_{n-1}]$ is (represented by) a permutation p of dom(a), and a function $d : (\Pi i : dom(a)) \rightarrow (C.D)(a(p(i)))$ . Equality of representations is modulo permutations.

It is as iff the angel has an inexhaustible supply of slave devices
to which she can issue as many commands in parallel as she likes
(possibly none). But she has to wait for all the responses.

What does one have to show about this? That C! is the free $\otimes$ comonoid generated by C? What is this in layman’s
terms?

]]>