Email Gateway (Aug 22 2022 at 13:35): Email Gateway (Aug 22 2022 at 13:35):From: Jørgen Villadsen <jovi@dtu.dk>
Hi,
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"?
OCaml does not have transparent ascription so perhaps the default for SML should be opaque ascription.
Thanks,
Jørgen
Email Gateway (Aug 22 2022 at 13:35):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Jørgen,
Hi,
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.
Cheers,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 13:35):From: Makarius <makarius@sketis.net>
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
signature.asc
Email Gateway (Aug 22 2022 at 13:35):From: David Matthews <dm@prolingua.co.uk>
Pretty-printing isn't part of the ML standard so it's not always clear
how to do it properly. There have been various changes over the years.
In particular, printing exception packets is difficult because the
packet can contain values of types that exist only where the exception
is raised. In the example below, "t" may not actually be exported from
the signature. So, Poly/ML puts the print function that applies where
the exception is raised into the exception packet and uses that if it
needs to print the packet. There are no plans to change this.
There have been some changes around the printing of types exported
through opaque matching. When a structure matches a signature
containing a type through opaque matching the semantics says that this
creates a new type "name". Poly/ML creates a new ref to hold the pretty
print function for the new type. Previously this was initialised to the
pretty print function for the implementing type but this was changed in
5.6.1 to default to printing "?". It later became clear that this was
too restrictive when the signature contained a datatype (e.g. "test"
below) so there was a further change in commit 29985b1c in git master.
So now if you install pretty printers both within the structure, (1)
below, for the exception, and outside the signature (2) it will work
as you expect.
David
Email Gateway (Aug 22 2022 at 13:36):From: Jørgen Villadsen <jovi@dtu.dk>
Thanks to Florian, Makarius and David for the explanations.
Jørgen
Email Gateway (Aug 22 2022 at 15:28):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Jørgen,
after revisting the matter of opaque ascription, I came to the
conclusion that the situation »as it is« seems to be fine:
a) Type abstraction works via datatypes with hidden (unexported)
constructors, which works regardless whether ascription is transparent
or opaque. An abstract type in Isabelle/HOL is never a mere type synonym!
b) The Isabelle/ML tradition has a bias towards transparent ascription.
Cheers,
Florian
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC