From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 369667EE51 for ; Mon, 29 Apr 2013 07:17:04 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of rathereasy@gmail.com) identity=pra; client-ip=209.85.128.169; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="rathereasy@gmail.com"; x-sender="rathereasy@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of rathereasy@gmail.com designates 209.85.128.169 as permitted sender) identity=mailfrom; client-ip=209.85.128.169; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="rathereasy@gmail.com"; x-sender="rathereasy@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-ve0-f169.google.com) identity=helo; client-ip=209.85.128.169; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="rathereasy@gmail.com"; x-sender="postmaster@mail-ve0-f169.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: At4BAPsAflHRVYCpm2dsb2JhbAA4Gg6DL6wuiWWINXcIFg4BAQEBAQYLCwkUKIIfAQEEAScZARsSCwEDAQsGBQsaISIBEQEFAQoSBhMSCYdoAQMJBgwvoCqMMYJ9g2IKGScDClmHXgEFDI1WgTQEB4NPA4kSjgyBJo4fFimDeF8cgS4 X-IPAS-Result: At4BAPsAflHRVYCpm2dsb2JhbAA4Gg6DL6wuiWWINXcIFg4BAQEBAQYLCwkUKIIfAQEEAScZARsSCwEDAQsGBQsaISIBEQEFAQoSBhMSCYdoAQMJBgwvoCqMMYJ9g2IKGScDClmHXgEFDI1WgTQEB4NPA4kSjgyBJo4fFimDeF8cgS4 X-IronPort-AV: E=Sophos;i="4.87,571,1363129200"; d="scan'208";a="12533644" Received: from mail-ve0-f169.google.com ([209.85.128.169]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 29 Apr 2013 07:17:03 +0200 Received: by mail-ve0-f169.google.com with SMTP id pa12so1307522veb.28 for ; Sun, 28 Apr 2013 22:17:01 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:x-received:in-reply-to:references:date:message-id :subject:from:to:cc:content-type; bh=QOqsyDTD/1NV4LHVC07xeLalLzcpeiCqg20le/w42kE=; b=BMMgRK6lmQ66eIuROsCd2De8j1h3utTqLXL0K9vUyoLOqfOSOBAvlFwJB3LI9XGUtv 1l+vwpJU2+WmiJU0vQkBhkh8U5CNN/POnP9Ib/V04fhsEpu0SDNou0ZBC4Jq0+WyjNsS bfp+tknWreh5BYO2ksLCJ44eBe8rZK/q65xmhaZDLBsxMs54qwJzdleEhwCUOD6HVw7Y RdUII+/FfnP/pH5vd4pdPRr78VEL7/f2bP0DVDjY52yLBgVkocE+9W/FVc15OtBKvRby NskeNEv/kfHAEtbKfDuv+NpW3tvtMuXVitoNxJqx20TWMO/cA0HNKs8MuxS/xYWzywNU N9ng== MIME-Version: 1.0 X-Received: by 10.52.89.229 with SMTP id br5mr1193494vdb.24.1367212621852; Sun, 28 Apr 2013 22:17:01 -0700 (PDT) Received: by 10.220.200.66 with HTTP; Sun, 28 Apr 2013 22:17:01 -0700 (PDT) In-Reply-To: <00C57DF0-C6F0-4EDE-8607-2155F3A17146@math.nagoya-u.ac.jp> References: <00C57DF0-C6F0-4EDE-8607-2155F3A17146@math.nagoya-u.ac.jp> Date: Sun, 28 Apr 2013 22:17:01 -0700 Message-ID: From: Jacques Le Normand To: Jacques Garrigue Cc: OCaML List Mailing Content-Type: multipart/alternative; boundary=20cf307f3762a8a23604db78fe95 Subject: Re: [Caml-list] Request for feedback: A problem with injectivity and GADTs --20cf307f3762a8a23604db78fe95 Content-Type: text/plain; charset=ISO-8859-1 Fully injective types are the norm. It would have been nice to have a "non injectivity" or "phantom type" annotation. Since phantom types are seldom used, beginners won't get confused. It might even help beginners understand the concept of a phantom type. 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 --20cf307f3762a8a23604db78fe95 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable
Fully injective types are the norm. It would have been nic= e to have a "non injectivity" or "phantom type" annotat= ion. Since phantom types are seldom used, beginners won't get confused.= It might even help beginners understand the concept of a phantom type.



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<= br> http://caml.inria.fr/mantis/view.php?id=3D5985

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 =3D
=A0 | Int : int ty
=A0 | Pair : 'a ty * 'b ty -> ('a * 'b) ty
=A0 | 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) =3D struct
=A0 =A0type _ ty =3D
=A0 =A0 | Int : int ty
=A0 =A0 | Pair : 'a ty * 'b ty -> ('a * 'b) ty
=A0 =A0 | 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 =3D struct type 'a t =3D unit end
module M =3D F(U)
let w =3D M.T M.Int
(* val w : int U.t M.ty *)
let w' =3D match w with M.T x -> x | _ -> assert false
(* val w' : '_a M.ty =3D 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 =A0type:

let f : type a. a M.ty -> int -> a =3D
=A0 fun w x -> match w with M.Int -> x | _ -> assert false;;
let g : int -> float =3D f w';;

If we look at the source of the problem, it lies in the fact U.t is not inj= ective.
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 i= s (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 =3D
=A0 | Int : int ty
=A0 | Pair : 'a ty * 'b ty -> ('a * 'b) ty
=A0 | 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 ocam= l),
can also trigger it.
And you don't need a functor to trigger it: once you know that two type= s are equal
in some scope, there are many ways to leak that information.

=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D
Here comes the request for feedback:

The fix is simple enough: we should track injectivity, and assume that abst= ract
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 ab= stract
types, a straightforward solution is to add injectivity annotations on type= parameters,
the same way it was done for variance:

=A0 type #'a t

would mean that t is injective.
This is implemented in branches/non-vanishing, in the subversion repository= .
=A0 =A0 =A0 =A0 svn checkout http://caml.inria.fr/svn/branches/non-vanis= hing
Note that in that branch Hashtbl.t in the standard library is marked as inj= ective.
This introduces some new syntax, and libraries have to be modified to benef= it,
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 imp= ossible
branches. That branch is completely experimental.


--
Caml-list mailing list. =A0Subscription management and archives:
ht= tps://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
<= br>
--20cf307f3762a8a23604db78fe95--