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 5E6337EEF6 for ; Wed, 3 Jun 2015 19:42:44 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of mandrykin@ispras.ru) identity=pra; client-ip=83.149.199.45; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="mandrykin@ispras.ru"; x-sender="mandrykin@ispras.ru"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of mandrykin@ispras.ru) identity=mailfrom; client-ip=83.149.199.45; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="mandrykin@ispras.ru"; x-sender="mandrykin@ispras.ru"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail.ispras.ru) identity=helo; client-ip=83.149.199.45; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="mandrykin@ispras.ru"; x-sender="postmaster@mail.ispras.ru"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0ArBQD7O29V/y3HlVNbgxBUXoMevRmDFoJlAoFEPBABAQEBAQEBgQqEIwEBBCMEEUARCxgCAgUWCwICCQMCAQIBRRMGAgEBiC0Jt1CjagELIIEhiiKEUzoWglKBRQWMQYsMhmaBbIYTj0Ukg3tsgkcBAQE X-IPAS-Result: A0ArBQD7O29V/y3HlVNbgxBUXoMevRmDFoJlAoFEPBABAQEBAQEBgQqEIwEBBCMEEUARCxgCAgUWCwICCQMCAQIBRRMGAgEBiC0Jt1CjagELIIEhiiKEUzoWglKBRQWMQYsMhmaBbIYTj0Ukg3tsgkcBAQE X-IronPort-AV: E=Sophos;i="5.13,548,1427752800"; d="scan'208";a="162627070" Received: from mail.ispras.ru ([83.149.199.45]) by mail2-smtp-roc.national.inria.fr with ESMTP; 03 Jun 2015 19:42:42 +0200 Received: from [10.10.2.183] (pluton2.ispras.ru [83.149.199.44]) by mail.ispras.ru (Postfix) with ESMTPSA id D102254006F for ; Wed, 3 Jun 2015 20:42:40 +0300 (MSK) Message-ID: <556F3C8D.4060708@ispras.ru> Date: Wed, 03 Jun 2015 20:42:37 +0300 From: Mikhail Mandrykin User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.7.0 MIME-Version: 1.0 To: caml-list@inria.fr References: <20150602100015.E87D67EEF7@sympa.inria.fr> <556E2CE1.9040801@bioquant.uni-heidelberg.de> <556F30D9.9010109@inria.fr> In-Reply-To: <556F30D9.9010109@inria.fr> Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit Subject: Re: [Caml-list] pattern matching on mapped lists On 06/03/2015 07:52 PM, Romain Bardou wrote: > On 03/06/2015 00:23, Nils Becker wrote: >> I find this syntax handy >> >> let [ii; jj] = List.map float_of_int [i; j] in >> ... do stuff with the floats >> >> because it avoids repeating the function call. The compiler lets this >> pass but warns that the matching is not exhaustive since [] is not >> matched. This actually can't happen if I'm not mistaken. So, is this >> considered good style, or is there a better idiomatic way to do multiple >> assignments? If yes, should this be an enhancement request for the type >> checker? >> >> n. > > The type-checker cannot find out that List.map returns a list of the > same size. I think it would require dependent types. Maybe some GADT > can encode this, but it would be a bit messy. > > If you use this idiom often, maybe you should define some map > functions on tuples, whose length is known at compile-time: > > let map2 f (x, y) = f x, f y > > let (ii, jj) = map2 float_of_int (i, j) in > ... > > Unfortunately you need to define map2, map3, map4... > > Cheers, > It seems GADT encoding mostly works here, but the absence of local opens in patterns and redefinition of [] constructor and [_; _] special syntax for lists currently makes the use of such encoding inconvenient e.g.: module Flist = struct type z = Z type 'a s = S of 'a type ('a, _) t = | Nil : ('a, z) t | :: : 'a * ('a, 'b) t -> ('a, 'b s) t let rec map : type a. _ -> (_, a) t -> (_, a) t = fun f -> function | Nil -> Nil | x :: xs -> f x :: map f xs end open Flist let a :: b :: c :: Nil = map ((+) 2) @@ 1 :: 2 :: 3 :: Nil;; (* Can't use Flist.[a; b; c] on both sides *) let d :: e :: Nil = map ((^) "2 + ") @@ "1" :: "2" :: Nil;; let g :: Nil = map ((+) 2) @@ 1 :: Nil;; Printf.printf "%d = %s = %d\n%!" a d g;; BTW, both features are already proposed as feature requests: https://github.com/ocaml/ocaml/pull/187 https://github.com/ocaml/ocaml/pull/76 Regards, Mikhail -- Mikhail Mandrykin Linux Verification Center, ISPRAS web: http://linuxtesting.org e-mail: mandrykin@ispras.ru