[isabelle] Value restriction in generated SML code

[Peter Lammich]

Hi,

I ran into a value-restriction problem with generated SML code. 
I thought the code generator is supposed to do unit-insertion
automatically.

Consider the following example. Here, the generated code for "test"
will fail due to the value restriction. Manual unit-insertion "test2"
fixes the problem. Interestingly, the generated Scala code is fine.

--
  Peter


theory Scratch 
  imports Main
begin

datatype ('a,'s) M = M (run: "'s ⇒ ('a × 's)")

definition "return x ≡ M (λs. (x,s))"
definition "bind m f ≡ M (λs. let (x,s) = run m s in run (f x) s)"
definition "get ≡ M (λs. (s,s))"
definition "put x ≡ M (λ_. ((),x))"

definition "test ≡ bind get put"
definition "test2 (_::unit) ≡ bind get put"

value "run test True"
(*
Error: Type (unit, 'a) m includes a free type variable
val test : (unit, 'a) m = bind get put
*)

value "run (test2 ()) True"
(* Works *)
export_code test checking SML (* Error *)
export_code test checking Scala (* Works *)

[Florian Haftmann]

Hi Peter,

I ran into a value-restriction problem with generated SML code. 
I thought the code generator is supposed to do unit-insertion
automatically.

no, it does not. It only eta-expands proper functions.

Unit insertion must be constructed explicitly, as in the following
canonical example by Lukas Bulwahn from around 2009 / 2010:

export_code "Predicate.bind" in SML

Hope this helps,
Florian