[Agda] Choice sequences and effects

[Bas Spitters]

Dear Peter,

A small addition. We have discussed this before.

For the sake of the discussion let's restrict to the choice sequences
of natural numbers. As a special case of your construction, and a
historical precursor, we have an inductive type K of encodings of
continuous endofunctions on N^N.
This was considered by Brouwer and later used by Kreisel and Troelstra
to give a syntactic translation of a language with choice sequences to
a language without. This is their `elimination of choice sequences'.
Moerdijk and van der Hoeven later showed that this translation is in
fact determined by a sheaf model, sheaves over the monoid K.
[ Van der Hoeven, G. & Moerdijk, I., 1984a, "Sheaf Models for Choice
Sequences", Annals of Pure and Applied Logic, 27, no. 1, 63-107]

One can hope that this, and a better understanding of sheaf models for
type theory, could help to build an interpreter for a language with
choice sequences to pure type theory.
Obviously, a lot still needs to be done, but I wanted to take this
opportunity to hint at how sheaf models for type theory could be
useful.

Best,

Bas

On Sat, Oct 8, 2011 at 9:25 PM, Peter Hancock <hancock at spamcop.net> wrote:
> There may be some people on the list interested in how to write
> input-output programs that actually do things, where the programs are
> terms in an Agda-like type theory.
>
> With all due diffidence, and apologies for being unclear,
> I think writing such programs is
> essentially programming with choice sequences of a generalised form.
>
> A generalised choice sequence lives in a type of the form (nu F s),
> ie. an instance of a coinductive family (nu F) of type Set^S = S -> Set
> where F is an functor on indexed sets : Set^S, and s is an index.
> The functor F must be container-like: a S-sorted signature in the
> form of an S-indexed container
>
>        S -> Fam^2 S
>
> with outermost index  C and innermost R, so the container
> has the form
>
>        s |-> (C s, c |-> (R s c, r |-> n s c r))
>
> In the most interesting case, F has the form G', which has
> the same type as G, but has a state space (1 + (Sigma : g.S)g.C s),
> with a special initial state inL () and a subsequent reversal of the roles C
> and R.  Essentially,
> the first player chooses the initial state, and then play proceeds with
> roles reversed.
>
> Temporarily at least, this seems to me a very reasonable model of
> external-world resources, like
> access to measurements of the external world's state, or a means to change
> it.
>
> I don't really kown what the practical implications of this view are. Maybe
> the IO-interface
> should be structured in terms of the I/O-resources (file storage, network,
> physical world, peripherals)
> a program may access.
>
> Hank
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>