how to upset the ocaml type system....

how to upset the ocaml type system....

[Pietro Abate]

hi all,

the other day I was looking for a fringe case to show me the worst
complexity of the type inference algorithm...

I think I found what I was looking for:

let x1 = fun x -> (x,x) 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
let x6 = fun y -> x5 ( x5 y ) in
let x7 = fun y -> x6 ( x6 y ) in
x7 ( fun z -> z ) ;;

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

pietro

ps: the example is from the paper "polymorphic unification and ML
typing" from kannellakis

-- 
++ Blog: http://blog.rsise.anu.edu.au/?q=pietro
++ 
++ "All great truths begin as blasphemies." -George Bernard Shaw
++ Please avoid sending me Word or PowerPoint attachments.
   See http://www.fsf.org/philosophy/no-word-attachments.html

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

[David Allsopp]

> 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

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

[Daniel de Rauglaudre]

Hi,

On Tue, Aug 28, 2007 at 11:18:50PM +1000, Pietro Abate wrote:

> the other day I was looking for a fringe case to show me the worst
> complexity of the type inference algorithm...

Interesting. To see the resulting time, I changed the code into:

  let f =
  let x1 = fun x -> (x,x) 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 z -> z ) ;;

(I stopped at x5 to have a correct answering time.)

Compiling with -i to display the resulting type:
   ocamlc -c -i t.ml

Oops... lines and lines and lines...
Mmm.... let's see:
   ocamlc -c -i t.ml | wc -l
   16385

-- 
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/

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

[Christophe Raffalli]

[-- Attachment #1.1: Type: text/plain, Size: 1048 bytes --]

Daniel de Rauglaudre a écrit :
> Hi,
>
> On Tue, Aug 28, 2007 at 11:18:50PM +1000, Pietro Abate wrote:
>
>   
>> the other day I was looking for a fringe case to show me the worst
>> complexity of the type inference algorithm...
>>     
>
> Interesting. To see the resulting time, I changed the code into:
>
>   let f =
>   let x1 = fun x -> (x,x) 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 z -> z ) ;;
>
>   
This is strange, it is problematic even with -rectypes while this is
not necessary if the subtypes are shared ... I already so ocaml
printing some types with sharing, so why is this not the case here ?
(I am using 3.09.2)

With pml I seem to get a polynomial
behavior (at least quadratic but probably cubic), I tested up to 9.
This is because the type of xi  is bigger and bigger (but linear in i)
and it is copied by the generalisation and particularisation for each i.

Christophe


[-- Attachment #1.2: Christophe.Raffalli.vcf --]
[-- Type: text/x-vcard, Size: 380 bytes --]

begin:vcard
fn:Christophe Raffalli
n:Raffalli;Christophe
org:LAMA (UMR 5127)
email;internet:Christophe.Raffalli@univ-savoie.fr
title;quoted-printable:Ma=C3=AEtre de conf=C3=A9rences
tel;work:+33 4 79 75 81 03
note;quoted-printable:Message sign=C3=A9 cryptographiquement avec pgp, la clef publique est sur=
	 subkeys.pgp.net
x-mozilla-html:TRUE
version:2.1
end:vcard


[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 252 bytes --]

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

[Oliver Bandel]

Zitat von Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr>:

> Daniel de Rauglaudre a écrit :
> > Hi,
> >
> > On Tue, Aug 28, 2007 at 11:18:50PM +1000, Pietro Abate wrote:
> >
> >
> >> the other day I was looking for a fringe case to show me the worst
> >> complexity of the type inference algorithm...
> >>
> >
> > Interesting. To see the resulting time, I changed the code into:
> >
> >   let f =
> >   let x1 = fun x -> (x,x) 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 z -> z ) ;;
> >
> >
> This is strange, it is problematic even with -rectypes while this is
> not necessary if the subtypes are shared ... I already so ocaml
> printing some types with sharing, so why is this not the case here ?
> (I am using 3.09.2)
[...]

Sorry, if I can't follow why this discussion was started.
Is this a purely-academic talk, or does it have any relevance
for programmers who want to solve a programming problem?

Where could the problem behind this kind of functions
occure in practical programming?

I tested the above code and it needed a lot of time
to execute in the toplevel. I stopped this then, before the
toplevel were ready.

I never had such a behavior of so long needed time
for any kind of code.
So I doubt that this is a problem that matters in the realworld.
But possibly I'm wrong. Can you please elaobrate on this?
Is this more than a academic mental exercise?

Ciao,
   Oliver

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

[Daniel de Rauglaudre]

Hi,

On Wed, Aug 29, 2007 at 04:58:16PM +0200, Oliver Bandel wrote:

> Where could the problem behind this kind of functions
> occure in practical programming?

This example is just academic. The resulting value of this example is
an enormous value composed of a tree of couples of couples of couples
of couples... (and so on, depending on the level), and all "leaves"
are the same identical function. No interest.

But this reminds that the algorithm of type inference is exponential of
exponential in number of created type variables. In most programs, many
of these type variables are identical, and the algorithm shares them
using references.

In this example, all created type variables are different. The result
is a very complicated type, unuseful in practice.

-- 
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/

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

[Christophe Raffalli]

[-- Attachment #1.1: Type: text/plain, Size: 1018 bytes --]


Dear list members,

I wrote:
> With pml I seem to get a polynomial
> behavior (at least quadratic but probably cubic), I tested up to 9.
> This is because the type of xi  is bigger and bigger (but linear in i)
> and it is copied by the generalisation and particularisation for each i.
>
>   
Sorry, this was wrong, the size of the type generated by the example is
a double exponential
without sharing (so it breaks around 5-6 in OCaml) and single
exponential if you share subtypes (then it breaks
for 11-12 in PML).

What I find strange is that even with -rectypes, OCaml does not discover
that it can share subtypes
(as my algorithm in pml does) for this example. May be there is a little
room for improvement for
the (theoretical) complexity of the algorithm in OCaml, but may be it is
useless in practice.

Christophe

PS: if you want to know more about pml, go to
http://www.lama.univ-savoie.fr/~raffalli/pml,
but do not use the tar archive it is outdated, use the darcs repository.


[-- Attachment #1.2: Christophe.Raffalli.vcf --]
[-- Type: text/x-vcard, Size: 380 bytes --]

begin:vcard
fn:Christophe Raffalli
n:Raffalli;Christophe
org:LAMA (UMR 5127)
email;internet:Christophe.Raffalli@univ-savoie.fr
title;quoted-printable:Ma=C3=AEtre de conf=C3=A9rences
tel;work:+33 4 79 75 81 03
note;quoted-printable:Message sign=C3=A9 cryptographiquement avec pgp, la clef publique est sur=
	 subkeys.pgp.net
x-mozilla-html:TRUE
version:2.1
end:vcard


[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 252 bytes --]