Datatype replication exposes hidden constructors

[JohnReppy]

Version

110.79

Operating System

• All
• Linux
• macOS
• Windows
• Other Unix

OS Version

No response

Processor

No response

Component

Core system

Severity

Major

Description of the problem

Problem: Datatype replication brings constructors into scope when it
should not, in particular when the constructors are hidden by either

1. a type constraint in a signature that is matched transparently or
2. abstype or
3. both of the above.

Additional comments:
In practice, this is a major failing of the type system.
This issue means that we can construct a theorem

|- false

in ProofPower with a valid SML program, as shown below, even though no
sequence of valid logical inferences can give such a theorem.

datatype z1 = datatype pp'Kernel.THM;
val Thm {level, theory, ...} = t_thm;
val false_thm = Thm {level = level, sequent = ([], %<%F%>%), theory =
theory};

Ironically, ProofPower is an LCF-style theorem prover. Interestingly,
ProofPower is still 'sound' because it builds with another SML compiler
that does not have this issue. So here is a case where the standardized
ML, allowing compiler redundancy, is of practical benefit.

Transcript

No response

Expected Behavior

No response

Steps to Reproduce

(* 1. Example with datatype made abstract by signature *)

signature TEST1 =
sig
type t
end

structure Test1 : TEST1 =
struct
datatype t = A | B
end

datatype z1 = datatype Test1.t;

(* Constructors for datatype t should not be accessible

• but are made visible by the datatype replication. *)

A = B; (* we can refer to A and B... )
A : Test1.t; ( ...and constuct values of type Test1.t *)

(* 2. Example with an abstype *)

abstype t2 = A of int | B of bool
with
end

datatype z2 = datatype t2;

A 4 : t2; (* we can construct values of type t2 *)

(* 3. Example with both follows below )
(
Transcript: The following example shows that certain abstract types
cannot guarantee properties of values. In the following example, the
SML type system should guarantee that Test3.destNat returns a natural
number because Test3.t values can be created from natural numbers only.
*)
signature TEST3 =
sig
type t
val mkNat : int -> t
val destNat : t -> int
end

structure Test3 : TEST3 =
struct
abstype t = Nat of int (* always non-negative *)
with
fun mkNat n = if n < 0 then raise Fail "negative" else Nat n
fun destNat (Nat n) = n
end
end

open Test3;

mkNat ~3; (* Fail: negative - can't create a negative natural )
destNat (mkNat 0); ( ok *)

datatype z3 = datatype Test3.t;

val x = Nat ~3; (* now we can create a negative natural *)

destNat x; (* val it = ~3 : int *)

Additional Information

No response

Email address

phil.clayton@lineone.net

Comments from smlnj-gforge

Original smlnj-gforge bug number 149

Submitted via web form by Phil Clayton phil.clayton@lineone.net on 2015-16-24 at 05:1600

Keywords: datatype replication abstract type constructor

comment by @dmacqueen on 2016-15-12 17:1500 +000 UTC

Fix committed for 110.81 (revision 4297). Added a new boolean field "stripped" in the DATATYPE constructor for ticking. This is true when a datatype has been matched to a simple type spec in signature matching, otherwise (default) false. Datatype replication causes an error when the right hand side is a stripped datatype.