Induction over types

Dawid Toton

Christopher L Conway
 Dirk Thierbach

Christopher L Conway
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:   (:) 
From:  Dirk Thierbach <dthierbach@g...> 
Subject:  Re: [Camllist] Induction over types 
On Jan 31, 2008 12:38 PM, Dawid Toton <d0@wp.pl> 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 pseudocode 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 listtypes 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 nonuniform 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 recordtype. 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