Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Code-Export: SML value restriction problem?

Email Gateway (Aug 22 2022 at 16:19):

From: Peter Lammich <lammich@in.tum.de>
Hi, I ran into the following problem, where a code generation to SML
produces invalid SML code:

theory Scratch
imports Main 
begin

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
fine:

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
limitation?

Email Gateway (Aug 22 2022 at 16:20):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Peter,

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.

Andreas

Last updated: Apr 27 2024 at 01:05 UTC