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.0 required=5.0 tests=AWL,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 CC74EBC6C for ; Thu, 31 Jan 2008 23:44:53 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAIHeoUfVpUAUemdsb2JhbACQHgEBCQgpgRaYRQ X-IronPort-AV: E=Sophos;i="4.25,287,1199660400"; d="scan'208";a="7491236" Received: from mail.gmx.net ([213.165.64.20]) by mail1-smtp-roc.national.inria.fr with SMTP; 31 Jan 2008 23:44:53 +0100 Received: (qmail invoked by alias); 31 Jan 2008 22:44:51 -0000 Received: from dialin-145-254-248-140.pools.arcor-ip.net (EHLO dialin-145-254-248-140.pools.arcor-ip.net) [145.254.248.140] by mail.gmx.net (mp024) with SMTP; 31 Jan 2008 23:44:51 +0100 X-Authenticated: #11134691 X-Provags-ID: V01U2FsdGVkX19pWu9d3vxpwv0fKKr3wJDFs6O6Ek4iGvOt37zsGe pVuhgX0o39g4z5 Received: from dirk by feanor.private-host.de with local (masqmail 0.2.20) id 1JKhC4-2xP-00 for ; Thu, 31 Jan 2008 22:43:36 +0100 Date: Thu, 31 Jan 2008 22:43:36 +0100 To: caml-list@yquem.inria.fr Subject: Re: [Caml-list] Induction over types Message-ID: <20080131214336.GA11358@feanor> References: <47A20799.4030706@wp.pl> <4a051d930801311018k6aa4b8bdge32400c6a36b9b78@mail.gmail.com> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <4a051d930801311018k6aa4b8bdge32400c6a36b9b78@mail.gmail.com> User-Agent: Mutt/1.5.6+20040523i From: Dirk Thierbach X-Y-GMX-Trusted: 0 X-Spam: no; 0.00; invokes:01 ocaml:01 'a-:01 node:01 node:01 non-uniform:01 recursive:01 constructors:01 recursion:01 recursive:01 quantifiers:01 ocaml:01 val:01 trie:98 trie:98 On Jan 31, 2008 12:38 PM, Dawid Toton wrote: > 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] You cannot do that directly, because the type system is not strong enough to make a connection between the actual value of "depth" and the number of list-types that must be nested inside the type for "lst". However, there are two ways to emulate this behaviour. The first is to define an ordinary algebraic data type. What you wanted is lists nested within lists, which is called a trie: type 'a trie = Leaf of 'a | Node of ('a trie) list let rec trie_map f = function | Leaf x -> Leaf (f x) | Node l -> Node (List.map (trie_map f) l) ;; let rec trie_rev = function | Leaf x -> Leaf x | Node l -> Node (List.rev_map trie_rev l) ;; let x = Node [Node [Leaf 1; Leaf 2]; Node [Leaf 3; Leaf 4]] Let's test: # trie_rev x;; - : int trie = Node [Node [Leaf 4; Leaf 3]; Node [Leaf 2; Leaf 1]] Ok, works. However, all these Node's and Leaf's are a bit unwieldy. So the other way use to define a non-uniform recursive type, by swapping the order of the type constructors inside a node. Let's rename them for clarity: type 'a deep_trie = Inner of 'a | Nest of ('a list) deep_trie But to deal with this type, we need what is called polymorphic recursion -- inside a recursive definition, the recursive function must still have the quantifiers, so it can be used for a different type. This can only work if the type is known in advance, and the only way to encode this into OCaml at the moment is with a record-type. That's a bit awkward, but I suppose a few macros could make this more readable. Let's look at actual code, with the wrapper lines arranged to be as unobtrusive as possible: type _deep_map = {_deep_map: 'a 'b. ('a -> 'b) -> 'a deep_trie -> 'b deep_trie} let deep_map = let rec poly = { _deep_map= let deep_map f = function | Inner x -> Inner (f x) | Nest l -> Nest (poly._deep_map (List.map f) l) in deep_map } in poly._deep_map;; type _deep_map_rev = {_deep_map_rev: 'a 'b. ('a -> 'b) -> 'a deep_trie -> 'b deep_trie} let deep_map_rev = let rec poly = { _deep_map_rev= let deep_map_rev f = function | Inner x -> Inner (f x) | Nest l -> Nest (poly._deep_map_rev (List.rev_map f) l) in deep_map_rev } in poly._deep_map_rev;; let deep_rev = deep_map_rev (fun x -> x) let y = Nest (Nest (Inner [[1;2]; [3;4]])) # deep_rev y;; - : int deep_trie = Nest (Nest (Inner [[4; 3]; [2; 1]])) Ok, works too. Now you need only to prefix your data with Nest (Nest (Nest ... (Inner ...))) with the appropriate number of levels. (Oh, and it will guarantee that your tree is the same number of levels everywhere, unlike the first data type.) > And how can I have arbitrary transposition: > > val transpose: int list -> 'a list -> 'a list This should also work with one of the above data types. HTH, - Dirk