From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 8A9FB81799 for ; Fri, 26 Jul 2013 19:15:52 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of mathieu.barbin@gmail.com) identity=pra; client-ip=209.85.216.42; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="mathieu.barbin@gmail.com"; x-sender="mathieu.barbin@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of mathieu.barbin@gmail.com designates 209.85.216.42 as permitted sender) identity=mailfrom; client-ip=209.85.216.42; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="mathieu.barbin@gmail.com"; x-sender="mathieu.barbin@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-qa0-f42.google.com) identity=helo; client-ip=209.85.216.42; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="mathieu.barbin@gmail.com"; x-sender="postmaster@mail-qa0-f42.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgACAK+t8lHRVdgqk2dsb2JhbABbhAu+bwgWDgEBAQEHCwsJFAQkglIZARseAxIJB10BEQEFAYgyAQMPmBqCfoxPgn+ERQoZJw1kh3QBBQyQDoNvA5dfj2cWKYRWIA X-IPAS-Result: AgACAK+t8lHRVdgqk2dsb2JhbABbhAu+bwgWDgEBAQEHCwsJFAQkglIZARseAxIJB10BEQEFAYgyAQMPmBqCfoxPgn+ERQoZJw1kh3QBBQyQDoNvA5dfj2cWKYRWIA X-IronPort-AV: E=Sophos;i="4.89,752,1367964000"; d="scan'208";a="22368867" Received: from mail-qa0-f42.google.com ([209.85.216.42]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 26 Jul 2013 19:15:51 +0200 Received: by mail-qa0-f42.google.com with SMTP id bv4so535079qab.1 for ; Fri, 26 Jul 2013 10:15:50 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:date:message-id:subject:from:to:content-type; bh=6ESPHxocTLaGZLLEs+XU27q/I12ELPcotSkTdLjkWIM=; b=YZvpTcgvmYEk+1bbXTFVADKKesMrMwhHi7ZI1/MZSgFvf+bhgTgo4saw71pKZG94cQ GvtOnKm2x0DAent5nV9Jar34kB8CSg97/lwU/kNbnrO8UFC39pwFLlJmnaYuFbniELeV oz4BOV3A0HjIionwDJh5MpVL+TdE9SiJknSyPAmLPVGqu+T2s86MeXcbhHKmo8jngruQ Buyinq9wFARwHRdIjNZ3GFk32JeNnIihXjqR6zGcWAPhJNOVLextgsdh9dG7DGGKv7t9 XwXxovuh91EJdOxXbYxqIYUSm9NGXG+eVHFzNVyKkpiASGs95hyFPT9cJ7QonzmBwNh5 kDdQ== MIME-Version: 1.0 X-Received: by 10.49.17.101 with SMTP id n5mr1876885qed.88.1374858950587; Fri, 26 Jul 2013 10:15:50 -0700 (PDT) Received: by 10.229.104.70 with HTTP; Fri, 26 Jul 2013 10:15:50 -0700 (PDT) Date: Fri, 26 Jul 2013 13:15:50 -0400 Message-ID: From: Mathieu Barbin To: caml-list@inria.fr Content-Type: multipart/alternative; boundary=047d7bea3e6a5dc21604e26d4b39 Subject: [Caml-list] GADT: question about inference --047d7bea3e6a5dc21604e26d4b39 Content-Type: text/plain; charset=ISO-8859-1 Hello, Playing around with a reduced version of a dynamic types, I ran into some type errors, and I feel that I'd love to understand more about the way the inference work: type _ ty = Int : int ty | String : string ty module H : sig type t val ty : t ty end = struct type t = int let ty = Int end (* from now, trying various implementation for [f] *) let f : H.t -> int = match H.ty with | Int -> (fun (a : H.t) -> (a : int)) | _ -> assert false ;; Error: This expression has type H.t but an expression was expected of type int let f : H.t -> int = fun (a : H.t) -> match H.ty with | Int -> (a : int) | _ -> assert false ;; Error: This expression has type H.t but an expression was expected of type int let f : H.t -> int = let aux : type a. a ty -> a -> int = function | Int -> (fun a -> a) | _ -> assert false in aux H.ty ;; (* val f : H.t -> int = *) I can't quite come up with a clear mental model of why in-lining the pattern matching in the first versions of [f]t would not type check. I tried adding some more type coercions without great success. I'd be very grateful to get some feed back about this restriction. Thanks, Mathieu --047d7bea3e6a5dc21604e26d4b39 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable
Hello,

Playing around with a reduce= d version of a dynamic types, I ran into some type errors, and I feel that = I'd love to understand more about the way the inference work:

ty= pe _ ty=A0 =3D Int : int ty | String : string ty

module H : sig
=A0 type t
=A0 val ty : t ty
end =3D struct
= =A0 type t =3D int
=A0 let ty =3D Int
end

(* from now, t= rying various implementation for [f] *)

let f : H.t -= > int =3D
=A0=A0=A0 match H.ty with
=A0=A0=A0 | Int -> (fun (a : H.t) -> (a = : int))
=A0=A0=A0 | _ -> assert false
=A0 ;;
Error: This expres= sion has type H.t but an expression was expected of type
=A0=A0=A0=A0=A0= =A0=A0=A0 int

let f : H.t -> int =3D fun (a : H.t) ->
=A0=A0=A0 match H.ty with
=A0=A0=A0 | Int -> (a : int)
=A0=A0=A0 |= _ -> assert false
=A0 ;;
Error: This expression has type H.t but = an expression was expected of type
=A0=A0=A0=A0=A0=A0=A0=A0 int

l= et f : H.t -> int =3D
=A0 let aux : type a. a ty -> a -> int = =3D function
=A0=A0=A0 | Int -> (fun a -> a)
=A0=A0=A0 | _ -> assert false=A0 in
=A0 aux H.ty
=A0 ;;

(* val f : H.t -> int =3D <= fun> *)

I can't quite come up with a clear mental = model of why in-lining the pattern matching in the first versions of [f]t w= ould not type check. I tried adding some more type coercions without great = success. I'd be very grateful to get some feed back about this restrict= ion.

Thanks,
Mathieu

=
--047d7bea3e6a5dc21604e26d4b39--