RE: [Caml-list] how to upset the ocaml type system....

["David Allsopp" <dra-news@metastack.com>]

> are there any other examples that exhibit worst-case complexity ?

let pair = fun x -> (fun y -> (fun z -> ((z x) y)))
in
  let x1 = fun y -> (pair y) y
  in
    let x2 = fun y -> x1 (x1 y)
    in
      let x3 = fun y -> x2 (x2 y)
      in
        let x4 = fun y -> x3 (x3 y)
        in
          let x5 = fun y -> x4 (x4 y)
          in
            x5 (fun y -> y);;

This one computes much faster (by which I mean the type checker does get
there in a few minutes!) but demonstrates the exponential blow-up of the
length of a type compared with the code it comes from (the type of this
expression 131070 lines long on my console...). It is translated from
http://www.cl.cam.ac.uk/teaching/2006/Types/typ.pdf p. 29 (Slide 25) which
is itself from Mairson, H. G. (1990). Deciding ML typability is complete for
deterministic exponential time. (In Proc. 17th ACM Symposium on Principles
of Programming Languages, pp. 382--401.)


David