Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Lazy Code Generation


view this post on Zulip Email Gateway (Jul 15 2021 at 12:57):

From: Simon Foster via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Dear all,

I've been experimenting with SML code generation for lazy evaluated
codatatypes using the theory Code_Lazy. It's a very nice development, and
it works pretty well on some examples. However, I've hit an issue with
generated code that seems to be related to polymorphism.

Consider the following example. First, I create the following codatatype
and set up the lazy code generator:

codatatype ('e, 'r) itree = Ret 'r | Tau "('e, 'r) itree" | Vis "'e ⇀ ('e,
'r) itree"
code_lazy_type itree

then I create a simple definition

definition deadlock :: "('e, 'r) itree" where "deadlock = Vis Map.empty"

Finally, I try to evaluate this, which invokes the code generator:

value "deadlock :: (int, int) itree"

This raises an error in the generated code:

Error: Type ('a, 'b) itree includes a free type variable
val deadlock : ('a, 'b) itree = Lazy_itree (Lazy.lazy (fn ... => ...))
At (line 155 of "generated code")
Error: Type error in function application.
Function: term_of_itree typerep_int term_of_int :
('a, inta) itree -> term
Argument: deadlock : ('a, 'b) itree
Reason: Can't unify inta to 'a (Cannot unify with explicit type variable)

There seems to be an issue with the polymorphic type of deadlock, which
cannot be specialised when used in another definition. I attach a minimal
example that exhibits this behaviour. I can code generate Haskell for this
example (excluding Code_Lazy) without issue. Moreover, if I turn itree into
a datatype (i.e. inductive) and don't use code_lazy_type, the code also
works correctly.

Is there a workaround for this issue?

Regards,

Simon.
Lazy.thy

view this post on Zulip Email Gateway (Jul 16 2021 at 09:29):

From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Dear Simon,

You're running into SML's value restriction, which is independent of codatatypes and
code_lazy. See http://users.cis.fiu.edu/~smithg/cop4555/valrestr.html for an explanation.
Deadlock's right-hand side consists of a number of function applications and is therefore
not a syntactic ML value. So SML will not treat it as a polymorphic value.

The standard way around is to introduce a unit closure:

definition deadlock :: "unit => ('e, 'r) itree" where "deadlock _ = Vis Map.empty"

Then export_code for deadlock results in a fun instead of a val and fun always is a
syntactic ML value. If you don't want to clutter your formalization with those unit
closures, you can also instruct the code generator's preprocessor to introduce those
closures. See the construction of Fail' in CryptHOL.Generative_Probabilistic_Value in the
AFP for a very similar example:

https://www.isa-afp.org/browser_info/current/AFP/CryptHOL/Generative_Probabilistic_Value.html

Hope this helps
Andreas


Last updated: Jul 15 2022 at 23:21 UTC