Induction over types

Induction over types

[Dawid Toton]

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

Re: [Caml-list] Induction over types

[Christopher L Conway]

Dawid,

Your example seems to require dependent types (e.g., "nested lists of
depth k") or runtime type inspection. Neither is directly supported by
OCaml (although there might be experimental extensions out there that
do what you want). You might be interested the "Scrap Your
Boilerplate" approach which is available in the latest versions of
Haskell (http://www.cs.vu.nl/boilerplate). I think this would
accomplish what you're asking. But it's implementation and use is
non-trivial.

Chris

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]
>
> 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
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>
>

Re: [Caml-list] Induction over types

[Dirk Thierbach]

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

Re: [Caml-list] Induction over types

[Christophe TROESTLER]

On Thu, 31 Jan 2008 22:43:36 +0100, Dirk Thierbach wrote:
> 
> 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.

Actually, a nice way to do the same and which is much more readable
(at heart, it is the very same solution) is to use recursive modules
(their semantic are not completely fixed but I guess the following
should work even in the future):

module rec Deep : sig
  type 'a trie = Inner of 'a | Nest of ('a list) trie
  val map : ('a -> 'b) -> 'a trie -> 'b trie
  val rev_map : ('a -> 'b) -> 'a trie -> 'b trie
end = struct
  type 'a trie = Inner of 'a | Nest of ('a list) trie
  let map f = function
    | Inner x -> Inner(f x)
    | Nest l -> Nest(Deep.map (List.map f) l)
  let rev_map f = function
    | Inner x -> Inner(f x)
    | Nest l -> Nest(Deep.map (List.rev_map f) l)
end;;

open Deep;;

> let y = Nest (Nest (Inner [[1;2]; [3;4]]))

# Deep.rev_map (fun x -> x) y;;
- : int Deep.trie = Nest (Nest (Inner [[4; 3]; [2; 1]]))

My 0.02€,
ChriS