Re: [Caml-list] Induction over types

[Dirk Thierbach <dthierbach@gmx.de>]

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 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