Re: [isabelle] Code-Export: SML value restriction problem?
Your feeling is right, this is an instance of the value restriction problem.
SOME (fn x => ...) is a syntactic value, so the declaration
val bar = SOME (fn x => ...)
is valid because syntactic values may be polymorphic. Conversely,
SOME (SOME o Product_Type.fst)
is not a syntactic value, so ML chokes upon the polymorphism.
On 27/10/17 04:21, Peter Lammich wrote:
Hi, I ran into the following problem, where a code generation to SML
produces invalid SML code:
definition "foo â Some (Some o fst)"
export_code foo checking SML
Â (*** ROOT.ML:7: error: Type ('a * 'b -> 'a option) option includes a
free type variable *)
When, however, unfolding the function composition, everything works
definition "bar â Some (Îx. Some (fst x))"
export_code bar checking SML
Â (* No error *)
What happened here? Is this a bug in the code generator, or a known
p.s. The generated Scala code is valid in both cases.
This archive was generated by a fusion of
Pipermail (Mailman edition) and