Home My Page Projects Code Snippets Project Openings SML/NJ Bugs
Summary Activity Tracker Lists

[#149] Datatype replication exposes hidden constructors

Date:
2015-11-24 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 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 *)
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 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.

Submitted via web form by Phil Clayton <phil.clayton@lineone.net>

Comments:

Message  ↓
Date: 2016-09-12 17:15
Sender: David MacQueen

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.

Attached Files:

Changes

Field Old Value Date By
status_idOpen2016-09-12 17:15dbm
close_dateNone2016-09-12 17:15dbm
ResolutionAccepted As Bug2016-09-12 17:15dbm
assigned_tonone2015-11-24 05:18jhr
detailsProblem: 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. Submitted via web form by Phil Clayton <phil.clayton@lineone.net> 2015-11-24 05:18jhr
ResolutionNone2015-11-24 05:18jhr
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 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 *) 2015-11-24 05:18jhr