From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: * X-Spam-Status: No, score=1.3 required=5.0 tests=SPF_FAIL autolearn=disabled version=3.1.3 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by yquem.inria.fr (Postfix) with ESMTP id 45053BC6C for ; Thu, 31 Jan 2008 18:38:45 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAPuWoUfAXQImh2dsb2JhbACQIgEBAQgKKZlF X-IronPort-AV: E=Sophos;i="4.25,286,1199660400"; d="scan'208";a="7482910" Received: from discorde.inria.fr ([192.93.2.38]) by mail1-smtp-roc.national.inria.fr with ESMTP; 31 Jan 2008 18:38:39 +0100 Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id m0VHcZc2012048 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Thu, 31 Jan 2008 18:38:38 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ah4FANmVoUfUTWUFWGdsb2JhbACQFQMBFAkICRaZRw X-IronPort-AV: E=Sophos;i="4.25,286,1199660400"; d="scan'208";a="6789878" Received: from mx1.wp.pl ([212.77.101.5]) by mail2-smtp-roc.national.inria.fr with ESMTP; 31 Jan 2008 18:38:38 +0100 Received: (wp-smtpd smtp.wp.pl 10681 invoked from network); 31 Jan 2008 18:38:35 +0100 Received: from phpdk6.ph.kcl.ac.uk (HELO [137.73.5.196]) (d0@[137.73.5.196]) (envelope-sender ) by smtp.wp.pl (WP-SMTPD) with AES256-SHA encrypted SMTP for ; 31 Jan 2008 18:38:35 +0100 Message-ID: <47A20799.4030706@wp.pl> Date: Thu, 31 Jan 2008 17:38:33 +0000 From: Dawid Toton User-Agent: Thunderbird 1.5.0.12 (X11/20071219) MIME-Version: 1.0 To: caml-list@inria.fr Subject: Induction over types Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-WP-AV: skaner antywirusowy poczty Wirtualnej Polski S. A. X-WP-SPAM: NO 0000000 [sfOE] X-Miltered: at discorde with ID 47A2079B.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; invokes:01 ocaml:01 'a-:01 val:01 val:01 ocaml:01 polymorphic:01 rec:01 rec:01 recursively:01 functions:01 int:01 int:01 arbitrary:02 match:02 I want to write a polymorphic function that invokes itself recursively, but with different types. For example I'd like to translate the following pseudo-code into OCaml: let rec deep_rev (lst:'a list) = List.rev (List.map (deep_rev:'a->'a) lst) let deep_rev (element:'a) = element (* initial induction step *) let rec super_wrap (depth:int) (lst:'a list) = match depth with | 0 -> lst | d -> super_wrap (d+1) [lst] And how can I have arbitrary transposition: val transpose: int list -> 'a list -> 'a list # transpose [2;0;1] [[[1;2];[3;4]] ;[[5;6];[7;8]] ] - : int list list list = [[[1; 3]; [5; 7]]; [[2; 4]; [6; 8]]] Do I have to have separate functions: val transpose1: int list -> 'a list -> 'a list (* identity *) val transpose2: int list -> 'a list list -> 'a list list val transpose3: int list -> 'a list list list -> 'a list list list ... But this is huge amount of redundant code! Here is for example my transpose3: http://www.toton.2-0.pl/OCaml/transpose.ml Dawid Toton