Re: [isabelle] Opaque ascription for SML code generation



On 12/06/16 15:01, Florian Haftmann wrote:
>> Is there a way to make the SML code generator use opaque ascription "structure Foo :> FOO = struct ... end" rather than transparent ascription "structure Foo : FOO = struct ... end"?
> 
> the short answer is, no.
> 
>> OCaml does not have transparent ascription so perhaps the default for SML should be opaque ascription.
> 
> The Isabelle/ML tradition prevers abstypes over opaque ascriptions – as
> far as I remember also pretty printing of values work better with
> abstypes than opaque ascriptions.  When signatures have been added to
> SML code generation, this pattern has been adopted.  Maybe it is time to
> revisit that.

See also
http://stackoverflow.com/questions/7296795/sml-whats-the-difference-between-using-abstype-and-using-a-signature-to-hide-t

After the Isabelle2016 release, we have discontinued SML/NJ and old
versions of Poly/ML, so there is a bit more flexibility now in canonical
patterns for Isabelle/ML.

The example with structure A3 from above is the difficult one, notably
the situation "does not work (overrides pp for int)". Defining the pp
outside of the structure basically works, but exceptions are not printed
correctly. This is how the problem with opaque ascription was discovered
many years ago, and the abstype solution took over.


Here is an update of the example A3 from Stackoverflow above, using
Isabelle2016 with its bundled Poly/ML 5.6:

ML ‹
structure A :>
sig
  type t
  exception BAD of t
  datatype test = Test of t
  val a: t
  val print: t -> string
end =
struct

type t = int

exception BAD of t
datatype test = Test of t

val a = 42

fun print i = "{" ^ Int.toString i ^ "}"

(*1*)
(*val _ = PolyML.addPrettyPrinter (fn _ => fn _ => fn x =>
PolyML.PrettyString (print x))*)
end;

(*2*)
(*val _ = PolyML.addPrettyPrinter (fn _ => fn _ => fn x =>
PolyML.PrettyString (A.print x))*)
›

ML ‹A.a; A.Test A.a; A.BAD A.a›


This leads to a mix of results, depending on the place where the pretty
printer is installed.

I still don't see how to get a simple and robust pretty printer setup,
so we can't use opaque ascription – unless David Matthews wants to
refine that again for a future release of Poly/ML.


	Makarius


Attachment: signature.asc
Description: OpenPGP digital signature



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