Date:
20151124 05:16 
Priority:
3 
State:
Closed 

Submitted by:
Bug Submitter (webuser)

Assigned to:
David MacQueen (dbm)

Machine Architecture: None 
Operating System: Generic Unix 
Component: Compiler 
Resolution: Fixed 
Severity: Major 
OS Version:

SML/NJ Version: 110.79 

Keywords: datatype replication abstract type constructor 
URL:


Transcript (of reproduction):

Source (for reproduction): (* 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 nonnegative *)
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 *)


Summary:
Datatype replication exposes hidden constructors 
Detailed description 
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 LCFstyle 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.
Submitted via web form by Phil Clayton <phil.clayton@lineone.net>

