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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id A94E47EE51 for ; Sun, 28 Apr 2013 07:54:20 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of rathereasy@gmail.com) identity=pra; client-ip=209.85.212.48; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="rathereasy@gmail.com"; x-sender="rathereasy@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of rathereasy@gmail.com designates 209.85.212.48 as permitted sender) identity=mailfrom; client-ip=209.85.212.48; receiver=mail2-smtp-roc.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 (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-vb0-f48.google.com) identity=helo; client-ip=209.85.212.48; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="rathereasy@gmail.com"; x-sender="postmaster@mail-vb0-f48.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AvcCAJi4fFHRVdQwk2dsb2JhbAA5Gg6DL6wtiWUBiDR2CBYOAQEBAQcLCwkUBCSCHwEBBAEnGQEbEgsBAwELBgULGiEiAREBBQEKEgYTEgmHaAEDCQYML6ERjDGCfYNrChknAwpZh14BBQyNVoE0BAeDTwOJEo4MgSaOHxYpg3hfHIEu X-IPAS-Result: AvcCAJi4fFHRVdQwk2dsb2JhbAA5Gg6DL6wtiWUBiDR2CBYOAQEBAQcLCwkUBCSCHwEBBAEnGQEbEgsBAwELBgULGiEiAREBBQEKEgYTEgmHaAEDCQYML6ERjDGCfYNrChknAwpZh14BBQyNVoE0BAeDTwOJEo4MgSaOHxYpg3hfHIEu X-IronPort-AV: E=Sophos;i="4.87,566,1363129200"; d="scan'208";a="15159535" Received: from mail-vb0-f48.google.com ([209.85.212.48]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 28 Apr 2013 07:54:19 +0200 Received: by mail-vb0-f48.google.com with SMTP id p12so320863vbe.35 for ; Sat, 27 Apr 2013 22:54:18 -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=0SuyeH57wBfKXn0S35dodRfxtluo7zGSDYBk4ivlRNE=; b=LW3U+MlgLyxVWfi+0bIUD1NnAtkAAAXWm7QDvdIHnijMqg+T6b7qLQSVKhRFEqmuKv 7CFrnX4m81aYYWtqU/isQtrk8F1J7qU6b4S1xX1n1zZj8k7xi6e/Y+L7eZCgxFDF9FOF P7i6f/7cjfQEeugV+fpEqeIOcoeD9RY9DxTC1jrIaaZeLXlDl0IFlRQMpOuB5JaBr4aA Xvp9RcihQF9MXyPgJXUYF2alHELvwPq12V4y2q/4XkPa2nCml+vTU/oxB9iUrXXGvT52 o5f4CvAOwGmqn0rGHDGFjfJKyRqKR7PC+uE714sIaBwXd6FeXok2S6vTuBFY2IgYx24/ vKvA== MIME-Version: 1.0 X-Received: by 10.52.229.234 with SMTP id st10mr26356229vdc.70.1367128458665; Sat, 27 Apr 2013 22:54:18 -0700 (PDT) Received: by 10.220.200.66 with HTTP; Sat, 27 Apr 2013 22:54:18 -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: Sat, 27 Apr 2013 22:54:18 -0700 Message-ID: From: Jacques Le Normand To: Jacques Garrigue Cc: OCaML List Mailing Content-Type: multipart/alternative; boundary=089e011822e824639304db656620 Subject: Re: [Caml-list] Request for feedback: A problem with injectivity and GADTs --089e011822e824639304db656620 Content-Type: text/plain; charset=ISO-8859-1 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 --089e011822e824639304db656620 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable
do we need the injectivity annotation at the parameter lev= el or at the type declaration level?

On Sat, Apr 27, 2013 at 5:02 PM, Jacques Garri= gue <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>
--089e011822e824639304db656620--