do we need the injectivity annotation at the parameter level or at the type
declaration level?


On Sat, Apr 27, 2013 at 5:02 PM, Jacques Garrigue <
garrigue@math.nagoya-u.ac.jp> wrote:

> Some of you may already be aware of PR#5985
> http://caml.inria.fr/mantis/view.php?id=5985
>
> To explain very shortly what is happening, a bug was found in the ocaml
> compiler, both 4.00 and the development version, such that one that
> convert a value from any type to any other type, bypassing all checks.
> This is what we call a soundness bug, a hole in the type system.
>
> Such problems happen at times, and we are usually very fast to fix them.
> However this time the problem is bit more subtle, because fixing it
> straightforwardly may make impossible to write a whole category of
> GADTs. Hence this request for feedback.
>
> Practical description of the problem:
>
> It is quite usual to write type witnesses using a GADT:
>
> type _ ty =
>   | Int : int ty
>   | Pair : 'a ty * 'b ty -> ('a * 'b) ty
>   | Hashtbl : 'a ty * 'b ty -> ('a, 'b) Hashtbl.t ty
>
> This looks fine, but now suppose that we write the following code:
>
> module F (X : sig type 'a t end) = struct
>    type _ ty =
>     | Int : int ty
>     | Pair : 'a ty * 'b ty -> ('a * 'b) ty
>     | T : 'a ty -> 'a X.t ty
> end
>
> The idea is to create a type witness with the
> type constructor X.t instead of Hashtbl.t.
> Now I can use it this way:
>
> module U = struct type 'a t = unit end
> module M = F(U)
> let w = M.T M.Int
> (* val w : int U.t M.ty *)
> let w' = match w with M.T x -> x | _ -> assert false
> (* val w' : '_a M.ty = M.Int *)
>
> What this means is that we can now give an arbitrary type
> to a witness for int. You can easily use it to build a function
> from int to any  type:
>
> let f : type a. a M.ty -> int -> a =
>   fun w x -> match w with M.Int -> x | _ -> assert false;;
> let g : int -> float = f w';;
>
> If we look at the source of the problem, it lies in the fact U.t is not
> injective.
> I.e. when we define a GADT, we assume that all the type variables in
> the return type can be determined from the type parameter.
> That is, from (int U.t M.ty) we assume that the type of the argument of T
> is (int M.ty).
> However, since U.t is not injective, int U.t is actually equal to any type
> 'a U.t,
> and we can convert.
> Note that, for known types, injectivity was already checked.
> I.e., the following definition is not accepted:
>
> type _ ty =
>   | Int : int ty
>   | Pair : 'a ty * 'b ty -> ('a * 'b) ty
>   | T : 'a ty -> 'a U.t ty
>
> However, abstract types were assumed to be injective.
> Here we see that you cannot take this for granted.
>
> The problem is of course not limited to type witnesses, and not even GADTs:
> types with constrained parameters (introduced at the very beginning of
> ocaml),
> can also trigger it.
> And you don't need a functor to trigger it: once you know that two types
> are equal
> in some scope, there are many ways to leak that information.
>
> =============================
> Here comes the request for feedback:
>
> The fix is simple enough: we should track injectivity, and assume that
> abstract
> types are not injective by default.
> However, this also means that the first type I defined above (using
> Hashtbl.t)
> will be refused.
>
> How many of you are using GADTs in this way, and how dependent are you on
> abstract types ?
>
>
> If we need to be able to define GADTs relying on the injectivity of some
> abstract
> types, a straightforward solution is to add injectivity annotations on
> type parameters,
> the same way it was done for variance:
>
>   type #'a t
>
> would mean that t is injective.
> This is implemented in branches/non-vanishing, in the subversion
> repository.
>         svn checkout http://caml.inria.fr/svn/branches/non-vanishing
> Note that in that branch Hashtbl.t in the standard library is marked as
> injective.
> This introduces some new syntax, and libraries have to be modified to
> benefit,
> so the question is do we really need it?
>
>
> Jacques Garrigue
>
> P.S.
> If you are curious about other difficulties of GADTs, the is also
> branches/abstract-new
> which introduces a notion of new types, either concrete or abstract, which
> are guaranteed
> to be distinct from each other, and any other concrete type. This is
> useful when
> checking the exhaustiveness of pattern-matching, as we can then discard
> impossible
> branches. That branch is completely experimental.
>
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs