caml-list - the Caml user's mailing list
 help / color / mirror / Atom feed
From: Mikhail Mandrykin <mandrykin@ispras.ru>
To: caml-list@inria.fr
Subject: Re: [Caml-list] pattern matching on mapped lists
Date: Wed, 03 Jun 2015 20:42:37 +0300	[thread overview]
Message-ID: <556F3C8D.4060708@ispras.ru> (raw)
In-Reply-To: <556F30D9.9010109@inria.fr>

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


  reply	other threads:[~2015-06-03 17:42 UTC|newest]

Thread overview: 5+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
     [not found] <20150602100015.E87D67EEF7@sympa.inria.fr>
2015-06-02 22:23 ` Nils Becker
2015-06-03 16:52   ` Romain Bardou
2015-06-03 17:42     ` Mikhail Mandrykin [this message]
2015-06-03 18:06       ` Octachron
2015-06-03 16:58   ` John Whitington

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=556F3C8D.4060708@ispras.ru \
    --to=mandrykin@ispras.ru \
    --cc=caml-list@inria.fr \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).