regression/polymorphic-recursion.sml

   1 datatype 'a t = R of 'a | L of 'a t t
   2
   3 val rec build: int -> int t =
   4    fn 0 => R 17
   5     | n => L (R (build (n - 1)))
   6
   7 val rec depth: int t -> int =
   8    fn R _ => 0
   9     | L (R z) => 1 + depth z
  10     | _ => raise Match
  11
  12 val n = depth (build 13)
  13 val _ =
  14    if n = 13
  15       then ()
  16    else raise Fail "bug"
  17
  18 (*
  19 val _ = R 13
  20 val _ = L (R (R 13))
  21
  22 val rec build: int -> int t =
  23    fn 0 => R 13
  24     | n => L (R (build (n - 1)))
  25
  26 val _ = f 13
  27   *)
  28 (*
  29
  30 val rec f =
  31    fn R _ => 0
  32     | L (R z) => 1 + f z
  33
  34 val v0: int t = R 13
  35 val v2: int t t = R v0
  36 val v1: int t = L (v2: int t t)
  37 val _ = L (L (R (R (R 13))))
  38 val _ = L (R (L (R (R 13))))
  39 val _ = L (L (R (R (R (R (R 13))))))
  40
  41    *)
  42
  43 (*
  44 datatype 'a t = A of 'a | B of ('a t * 'a t) t
  45 val v1 = A 13
  46 val v2 = A (v1, v1)
  47 val v3 = A (v2, v2)
  48 val v4 = B v3
  49 val v5 = B v4
  50
  51 val x = A 1 : int t
  52
  53 val y = B (A (x, x))
  54
  55 val z = B (A (y, y))
  56
  57 val a = B (A (z, z))
  58
  59 fun d ((A _) : 'a t) : int      = 0
  60   | d ((B (A (x, _))) : 'a t) : int = 1 + d x
  61
  62 val n = d a
  63 *)
  64
  65
  66 (*
  67
  68  Here's (the relevant part of) what the monomorphiser in smlc returns
  69 for your program.
  70
  71 datatype t_0 = B_0 of t_1 | A_0 of int
  72      and t_1 = A_1 of (t_0 * t_0)
  73
  74 It figures out exactly your observation that every use of B must be
  75 followed by A.
  76
  77 [z0 = int t]
  78 datatype z0 = A of int | B of z1
  79
  80 [z1 = (z0 * z0) t]
  81 datatype z1 = A of z0 * z0 | B of z2
  82
  83 [z2 = (z1 * z1) t]
  84 datatype z2 = A of z1 * z1 | B of z3
  85
  86 [z3 = (z2 * z2) t]
  87
  88
  89
  90
  91 B z1
  92 B (B z2)
  93 B (B (A (z1, z1)))
  94 B (B (A (A (z0,z0), A (z0,z0))))
  95
  96 B (B (A (A (v1, v1), A (v1, v1))))
  97
  98 B (B (A (A (v1, v1), A (v1, v1))))
  99
 100
 101
 102 datatype z = A of int | B of (z * z) t
 103 datatype w = A of z * z | B of (w * w) t
 104
 105 *)