[Axiom-developer] Re: Literate programming and Provisos

[Stephen Wilson]

Ralf Hemmecke <address@hidden> writes:

> > One can think of a continuation is an abstract object representing the
> > remainder of a computation.  We normally think about functions
> > returning values, with continuations we pass the value to the
> > remainder of the computation.
> 
> Oh, are you trying to say that in order to pass some value to the
> continuation, I don't need to know what the ongoing computation
> actually does? How do you think that fits in a typed environment like
> Spad/Aldor?

The basic issue in terms of typing continuation uses the property
that the continuation does not return (so does not have a type, per
say).  Strongly typed languages take different approaches to dealing
with these types of things.  Consider how Aldor, for example, deals
with goto, return, etc, by declaring the terms to have type Exit with
special rules to unify that type within a local context.

A similar approach may be possible in Spad/Aldor, but there is
certainly work to be done.  Im going to look at `Typing First-Class
Continuations in ML':
 
  http://portal.acm.org/citation.cfm?id=99608

ML most certainly has a strong/static type system with interesting
connections with Spad/Aldor (the module system and functors).  I see
no reason at this point to think that continuations cant play
gracefully with Spads type system.

> > It is common to have a continuation
> > represented explicitly as an argument.  In Spad or Aldor, this might
> > be written as:
> >  add-cc (c : Continuation(Integer), n : Integer) : Integer ==
> >     c(n + 1)
> 
> The first think that came to my mind when I saw that was to represent
> 
> Continuation(Integer)
> 
> by something like
> 
> Integer -> Generator(SomeType)
> 
> where SomeType for your example above would be Integer, but as you
> said, a continuation is not a function so its return type is rather
> unclear.

Even though a continuation does not return, that does not preclude the
possibility of assigning a meaningful type.

Note that a generator is not equivalent to a continuation, it is a
special case of what you can express using continuations as
primitives.  There are several online tutorials about continuations in
various languages.  I think Scheme is a good place to explore the
idea.  Perhaps the following might be a decent place to start:

  http://community.schemewiki.org/?call-with-current-continuation


> So how could (for your code) the compiler check that c(n+1) is indeed
> of type Integer (as add-cc claims). Continuation(Integer) says
> something about the input argument, but not about some return type.

I gave add-cc the type Integer because add-cc is not under any
obligation to call the continuation.  It could return like any other
function.

> Anyway, even if I could model some continuation by
> 
> INTYPE -> Generator(OUTTYPE)
> 
> there is an issue with destructiveness. Aldor/Spad is not a functional
> language. So if c is a continuation and I call
> 
> foo(c); bar(c);
> 
> then usually bar doesn't get the some "continuation" as foo gets,
> since foo might change that computation destructively (as is usually
> the case for Generator in Aldor).

I am not sure I follow.  I would imagine that a continuation in
Spad/Aldor would be an opaque object not subject to any kind of
destructive operation.  The `change in computation' as you witness in
Aldors Generator domain, can be viewed as a result of forming a
closure over some set of continuations, one of which is `current'.  A
generator is not a continuation, its a function+closure over the next
path of computation.


I hope some of this is clear.  Perhaps I can think of a meaningful
syntax for these ideas in Spad/Aldor and give an example of how a
Generator could be defined in terms of continuations, type system
technicalities not withstanding.


Thanks,
Steve