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 78E3B7FA5E for ; Wed, 19 Apr 2017 12:41:16 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=asai@is.ocha.ac.jp; spf=Pass smtp.mailfrom=asai@is.ocha.ac.jp; spf=None smtp.helo=postmaster@web.is.ocha.ac.jp Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of asai@is.ocha.ac.jp) identity=pra; client-ip=133.65.64.10; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="asai@is.ocha.ac.jp"; x-sender="asai@is.ocha.ac.jp"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of asai@is.ocha.ac.jp designates 133.65.64.10 as permitted sender) identity=mailfrom; client-ip=133.65.64.10; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="asai@is.ocha.ac.jp"; x-sender="asai@is.ocha.ac.jp"; 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@web.is.ocha.ac.jp) identity=helo; client-ip=133.65.64.10; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="asai@is.ocha.ac.jp"; x-sender="postmaster@web.is.ocha.ac.jp"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AqEUu9hKyQ/cb3UFJjNmcpTZWNBhigK39O0sv0rFi?= =?us-ascii?q?tYgRKvzxwZ3uMQTl6Ol3ixeRBMOAuq4C07KempujcFRI2YyGvnEGfc4EfD4+ou?= =?us-ascii?q?JSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgpp?= =?us-ascii?q?POT1HZPZg9iq2+yo9ZDeZwpFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+?= =?us-ascii?q?RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLd?= =?us-ascii?q?QgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8qhrUgflhi?= =?us-ascii?q?kHOTAn7W/ZicN/g75Grx2vvBF/xpLYbZuPOfZiZK7RY9UXTndBUMZLUCxBB5ux?= =?us-ascii?q?YY4RAOoHPOZXs4n9p1oTphaiHgmjHuLvwSJPi3Dsxq01yeUhHBrH3Aw7Bd4Ot2?= =?us-ascii?q?jbrNXvO6sIS++60LPEzTfbb/5P3zr29YvGcgg5rP2RU799f9DdxEgvGg/fj1id?= =?us-ascii?q?ppbpMy6J2ugVrmSX8vRsWfiyh2Mpqgx9uDmiy8c2hoXXmI4YxVbJ/jhjzokvP9?= =?us-ascii?q?23Ukt7bMakEJROsyGaMJN7Q808TG5zoio6y6YGtYS8fCcWyJQo3QTTZOabfISS?= =?us-ascii?q?4BLjTP6dITZ+hH17ZLKynwu+/Eaux+HmV8S50ExGoytKn9XWq3wBywTf6s2dRf?= =?us-ascii?q?t8+keh1yyP1wfW6uxcO080jrDUK586z74xjZofq0PDETP2mErslqOZbFkr9vKq?= =?us-ascii?q?6+T/ernmvIOTN5doigHiNaQjgtCwDv49MggKRmSb/eW81Kb//UDiW7VLjvg2kr?= =?us-ascii?q?HDv5zAJMQboLS5Aw5P3Yo55Ra/FWTu7NNNlnACKBdBeQmbp4nvIVDHZv7iXtml?= =?us-ascii?q?hFH5szptxvvGP/XIGZzMZizKi77gVbdmrUlXyAN1xNsZ5YoCWeJJG+76RkKk7I?= =?us-ascii?q?+QNRQ+KQHhm+s=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BoAwDAPfdYfwpAQYVcHhgHBgYYDYN3g?= =?us-ascii?q?QuOb6hhASOJfkMUAQEBAQEBAQEBAQESAQELFl2CMyCCcERKNAUgAQUBik0BmmK?= =?us-ascii?q?DRT+NcDqHcRqDJAELARYPEpBagmiCMQWHKQeCFYc8hTuGcYFWgiiCEXaLXA2CV?= =?us-ascii?q?YgJg3+CbpJIM4EVNoEmJh0ILYc4ZokVAQEB?= X-IPAS-Result: =?us-ascii?q?A0BoAwDAPfdYfwpAQYVcHhgHBgYYDYN3gQuOb6hhASOJfkM?= =?us-ascii?q?UAQEBAQEBAQEBAQESAQELFl2CMyCCcERKNAUgAQUBik0BmmKDRT+NcDqHcRqDJ?= =?us-ascii?q?AELARYPEpBagmiCMQWHKQeCFYc8hTuGcYFWgiiCEXaLXA2CVYgJg3+CbpJIM4E?= =?us-ascii?q?VNoEmJh0ILYc4ZokVAQEB?= X-IronPort-AV: E=Sophos;i="5.37,220,1488841200"; d="ml'?scan'208";a="269564524" Received: from web.is.ocha.ac.jp ([133.65.64.10]) by mail2-smtp-roc.national.inria.fr with ESMTP; 19 Apr 2017 12:41:14 +0200 Received: from mail-pf0-f197.google.com (mail-pf0-f197.google.com [209.85.192.197]) by web.is.ocha.ac.jp (Postfix) with ESMTP id 4ABC72011517B for ; Wed, 19 Apr 2017 19:41:12 +0900 (JST) Received: by mail-pf0-f197.google.com with SMTP id c2so10245578pfd.9 for ; Wed, 19 Apr 2017 03:41:12 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:date:from:to:subject:message-id:mime-version :content-disposition:user-agent; bh=9Vhim8VUKhzH8MKA48LTHQRQJQ3Lh6S4n7e8/sPBFCg=; b=MpTh88RFMJKR7Vb32gEgYFSw+uDt3/vpXfR69T0mgYAZPT6WcKkNa8iBi7AvdNJpB+ oiO8KR4OEEYThxRe/L0/AR48jIkJ99TtM7jblmrakEvnCuvaUIayQ/RTwBgBfvfva47K GkaQ6A/VdKK/YsUAAWEiRh+GG48civwmw5OAL5PQKatLkekmr6CJ+4qR3YsOrctGD9hb rE3AsTOlszy9kWRgsaJXnN/lD3G0eGTbtoFMIOuH5m1zJbFoW/HVppVdqfSxKo64DXrE Syked4wrJTC66kS4g/FqsIrd88za3jqM+S5oXOas7LDhB3iRRge6EO2XerBCBbsvXPk4 +5lw== X-Gm-Message-State: AN3rC/5xRp/PtB4diVNrTLkBYb5bPX1EGgFPqmxOosLEI7d/a0Kp1Gdl cmIx9qadfC2EghXpRkwACB7R61mSdH/Yh90I2rl8yASyb01esj9Hli0Yau7UO3B+M9pi1Crtf5c drcQ= X-Received: by 10.99.188.2 with SMTP id q2mr2490601pge.72.1492598471639; Wed, 19 Apr 2017 03:41:11 -0700 (PDT) X-Received: by 10.99.188.2 with SMTP id q2mr2490587pge.72.1492598471476; Wed, 19 Apr 2017 03:41:11 -0700 (PDT) Received: from localhost (112.136.65.224.er.eaccess.ne.jp. [112.136.65.224]) by smtp.gmail.com with ESMTPSA id s65sm3846207pgb.34.2017.04.19.03.41.10 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 19 Apr 2017 03:41:10 -0700 (PDT) Date: Wed, 19 Apr 2017 19:40:58 +0900 From: Kenichi Asai To: caml-list@inria.fr Message-ID: <20170419104058.GA63988@pllab.is.ocha.ac.jp> MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="h31gzZEtNLTqOjlF" Content-Disposition: inline User-Agent: Mutt/1.7.2 (2016-11-26) Subject: [Caml-list] Question on "more general" --h31gzZEtNLTqOjlF Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Dear OCaml type inference experts, If I infer the type (using Typemod.type_structure) of: let a = 1 in fun x -> 1 and see if the type of x is more general (using Ctype.moregeneral) than the type of a type variable (Btype.newgenvar ()), I obtain yes (since the type of x is 'a which is more general (or equal) than a newly created type variable, I guess). If I do the same for: let a = assert false in fun x -> 1 I obtain no, although it still seems that the type of x is the same 'a. (See attached file for the concrete program I executed. I used OCaml 4.04.0.) Why? Thank you in advance! -- Kenichi Asai --h31gzZEtNLTqOjlF Content-Type: text/plain; charset=us-ascii Content-Disposition: attachment; filename="main.ml" open Asttypes open Ast_helper open Types open Typedtree open Parsetree (* some helper functions *) (* extract_typ : Typedtree.structure -> type_expr *) let extract_typ str = match str.str_items with [{str_desc = Tstr_eval ({ exp_type = typ }, _)}] -> typ | _ -> failwith "cannot happen" (* split_arrow : type_expr -> type_expr * type_expr *) let rec split_arrow typ = match typ.desc with Tarrow (_, t1, t2, _) -> (t1, t2) | Tlink (typ') -> split_arrow typ' | _ -> failwith "cannot happen" (* various expressions *) (* 1 *) let one : expression = Exp.constant (Const.integer "1") (* false *) let ff : expression = Exp.construct (mknoloc (Longident.Lident "false")) None (* variable pattern *) let var x : pattern = Pat.var (mknoloc x) (* fun x -> 1 *) let fun_x_one : expression = Exp.fun_ Nolabel None (var "x") one (* let a = 1 in fun x -> 1 *) let exp1 : expression = Exp.let_ Nonrecursive [Vb.mk (var "a") one] fun_x_one let env : Env.t = Env.initial_safe_string (* infer type of exp1 *) let (str1', _, _) = Typemod.type_structure env [Str.eval exp1] Location.none (* type of x *) let (typx1, _) = split_arrow (extract_typ str1') let b1 = Ctype.moregeneral env false typx1 (Btype.newgenvar ()) ;; print_endline (if b1 then "true" else "false") (* assert false *) let assert_false : expression = Exp.assert_ ff (* let a = assert false in fun x -> 1 *) let exp2 : expression = Exp.let_ Nonrecursive [Vb.mk (var "a") assert_false] fun_x_one (* infer type of exp2 *) let (str2', _, _) = Typemod.type_structure env [Str.eval exp2] Location.none (* type of x *) let (typx2, _) = split_arrow (extract_typ str2') let b2 = Ctype.moregeneral env false typx2 (Btype.newgenvar ()) ;; print_endline (if b2 then "true" else "false") --h31gzZEtNLTqOjlF Content-Type: text/plain; charset=us-ascii Content-Disposition: attachment; filename=Makefile run : main ./main main : main.ml ocamlfind ocamlc -package compiler-libs.common,compiler-libs.bytecomp -linkpkg main.ml -o main clean : rm main main.cmi main.cmo --h31gzZEtNLTqOjlF--