Re: [isabelle] interpreters and continuations



Unfortunately, code generation does not currently work for HOLCF definitions.

This is also on our to-do list. I plan to bring this up at the next Isabelle developer's meeting this summer, if it hasn't been dealt with before then. Implementing it will take some coordinated effort between the HOLCF people (mainly me) and the code generation people (mainly Florian Haftmann).

Of course, if users are clamoring for this new feature, it might encourage us to implement it sooner...

- Brian

Quoting Jeremy Siek <jeremy.siek at gmail.com>:

Good to hear.

Does the code generation support work for HOLCF fixrec
definitions?

Cheers,
Jeremy

On Wed, Mar 4, 2009 at 9:22 AM, Brian Huffman <brianh at cs.pdx.edu> wrote:
Certainly, using the HOLCF continuous function type should allow you to
define datatypes with continuations, just like you would define them in
Haskell or ML. The domain package currently allows you to use indirect
recursion with the continuous function space; for example, you can declare
types like this:

domain 'a foo = Foo "(foo -> 'a) -> 'a" | Bar 'a

Currently, support for indirect recursion is rather limited (you can't use
indirect recursion with arbitrary type constructors, due to soundness
concerns), and the domain package doesn't give you a very useful induction
rule for such types. But I am working on some big improvements; the support
for indirect recursion should get much better within the next few months.

- Brian


Quoting Tobias Nipkow <nipkow at in.tum.de>:

Not in HOL (or other logics of total functions), but in the extension
HOLCF, which supports a separate type of continuous functions. I am not
sure if HOLCF has been used for this purpose before.

Tobias

Jeremy Siek schrieb:

Lately I've been investigating writing interpreters in Isabelle/HOL and
ran into a problem when trying to support first-class continuations. The
typical approach when writing an interpreter in ML or Haskell is to
write the interpreter in continuation passing style (or monadic style)
and to embed the continuations as functions in the value (or expression)
datatype. Of course, in Isabelle/HOL this is not possible.

Using alternative approaches, such as SOS or abstract machines, this is
not
a problem because continuations are represented explicitly as data.

At this point I'm thinking that one can't write an interpreter in
Isabelle
that supports first-class continuations, but perhaps I'm  overlooking
something?

Cheers,
Jeremy












--
____________________________________
Jeremy Siek <jeremy.siek at colorado.edu>
http://ecee.colorado.edu/~siek/
Assistant Professor
Dept. of Electrical, Computer, and Energy Engineering
University of Colorado at Boulder











This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.