[Caml-list] Turning off type-checking

[Caml-list] Turning off type-checking

[Markus Mottl]

Hello,

people have always kept telling me that I have perverse needs, but that's
the way it is: I (ab)use OCaml for interpreting models learnt by a machine
learning system. The problem is that such models may require hundreds
of thousand lines of OCaml-code including absolutely mad amounts of
pattern-matches on and constructions of values of sum- and product type.

Needless to say that I get into trouble when I actually want to interpret
or compile these models to evaluate them on new data. Type checking just
takes an awful amount of time, in fact much longer than the learning
algorithm needs for model generation...

It would be really nice if there were some command-line flag for the
OCaml-compilers which turns off every check that is not required under the
assumption that the given OCaml-code is (type) correct as is guaranteed in
my case. Would this be easily possible? What else could I do to reduce the
amount of work the OCaml-compiler has to do? Insert Obj.magic everywhere?

Best regards,
Markus

-- 
Markus Mottl                                             markus@oefai.at
Austrian Research Institute
for Artificial Intelligence                  http://www.oefai.at/~markus
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Turning off type-checking

[Lauri Alanko]

> It would be really nice if there were some command-line flag for the
> OCaml-compilers which turns off every check that is not required under the
> assumption that the given OCaml-code is (type) correct as is guaranteed in
> my case. Would this be easily possible? What else could I do to reduce the
> amount of work the OCaml-compiler has to do? Insert Obj.magic everywhere?

How about enabling -rectypes, defining

type t = t -> t

, casting everything to t with Obj.magic and then operating with this
pseudo-typeless language, and finally casting the values back to their real
types? Then at least you can do function application without casting all the
time.


Lauri Alanko
la@iki.fi
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Turning off type-checking

[Berke Durak]

On Mon, May 13, 2002 at 03:31:02PM +0200, Markus Mottl wrote:
> Hello,

Hi
 
>...
>
> Needless to say that I get into trouble when I actually want to interpret
> or compile these models to evaluate them on new data. Type checking just
> takes an awful amount of time, in fact much longer than the learning
> algorithm needs for model generation...

I'm conservatively assuming that your code uses just classical types
(guessing that type-checking objects etc. can be more costly).

Could the type experts on this list confirm or deny that :
	- For ``classical'' types, type-checking amounts to term unification.
	- Term unification can be done in worst-case linear-time.
	- Ocaml's unification algorithm is worst-case suboptimal.
	- This explains the ``awful amount of time'' needed for type checking.

If these are true, a fifth question arises :
	- Is it worth to make Ocaml's type checking worst-case optimal ? How will
this affect real average-case performance ?
-- 
Berke Durak
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Turning off type-checking

[Oliver Bandel]

On Mon, 13 May 2002, Markus Mottl wrote:

> Hello,
> 
> people have always kept telling me that I have perverse needs, but that's
> the way it is: I (ab)use OCaml for interpreting models learnt by a machine
> learning system. The problem is that such models may require hundreds
> of thousand lines of OCaml-code including absolutely mad amounts of
> pattern-matches on and constructions of values of sum- and product type.
[...]
> It would be really nice if there were some command-line flag for the
> OCaml-compilers which turns off every check that is not required under the
> assumption that the given OCaml-code is (type) correct
[...]

use Perl;

Ciao,
   Oliver

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Turning off type-checking

[Jacques Garrigue]

From: Markus Mottl <markus@oefai.at>

> people have always kept telling me that I have perverse needs, but that's
> the way it is: I (ab)use OCaml for interpreting models learnt by a machine
> learning system. The problem is that such models may require hundreds
> of thousand lines of OCaml-code including absolutely mad amounts of
> pattern-matches on and constructions of values of sum- and product type.
> 
> Needless to say that I get into trouble when I actually want to interpret
> or compile these models to evaluate them on new data. Type checking just
> takes an awful amount of time, in fact much longer than the learning
> algorithm needs for model generation...
> 
> It would be really nice if there were some command-line flag for the
> OCaml-compilers which turns off every check that is not required under the
> assumption that the given OCaml-code is (type) correct as is guaranteed in
> my case. Would this be easily possible? What else could I do to reduce the
> amount of work the OCaml-compiler has to do? Insert Obj.magic everywhere?

Unfortunately, the ocaml compiler is itself dependant on type
information.  Compilation of pattern-matching in particular is tightly
integrated with the type checker. So you cannot turn off type
checking, lest you get invalid code.

One thing you might want to try is to write your own interpreter for
your subset of ocaml. According to the code snippets you posted, it is
restricted enough, so that should be easy. Then you can experiment
without compiling, and compile later if you really need to. Note that
with some tricks your interpreter can share data representation with
ocaml, so that your functions could be called directly from ocaml
(with a bit of magic, of course).

As long as your type are not really huge (like in Alain's example),
and you are not using subtyping, I don't think that there is much room
for improvement in the compiler.  This said, we find a complexity bug
once in a while. One of them was quite serious: type checking was done
twice for arguments in applications. Usually you won't notice it, but
if you have an application inside an argument inside an
argument... this was exponential! Unfortunately I don't remember
whether this was corrected before or after 3.04.

Cheers,

Jacques Garrigue
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Turning off type-checking

[Markus Mottl]

On Tue, 14 May 2002, Jacques Garrigue wrote:
> One thing you might want to try is to write your own interpreter for
> your subset of ocaml. According to the code snippets you posted, it is
> restricted enough, so that should be easy. Then you can experiment
> without compiling, and compile later if you really need to.

Being so lazy, I thought that I could skip writing an interpreter,
because I needed a pretty-printer anyway. And OCaml-code is just fine
for this purpose...

> Note that with some tricks your interpreter can share data
> representation with ocaml, so that your functions could be called
> directly from ocaml (with a bit of magic, of course).

This is an interesting suggestion, thanks!

> As long as your type are not really huge (like in Alain's example), and
> you are not using subtyping, I don't think that there is much room for
> improvement in the compiler.  This said, we find a complexity bug once
> in a while. One of them was quite serious: type checking was done twice
> for arguments in applications. Usually you won't notice it, but if you
> have an application inside an argument inside an argument... this was
> exponential! Unfortunately I don't remember whether this was corrected
> before or after 3.04.

I don't think that I really hit the exponential wall anywhere so it's
probably just that type-checking takes much longer than I had expected.
Well, I can live with it...

Regards,
Markus Mottl

-- 
Markus Mottl                                             markus@oefai.at
Austrian Research Institute
for Artificial Intelligence                  http://www.oefai.at/~markus
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Turning off type-checking

[John Prevost]

>>>>> "mm" == Markus Mottl <markus@oefai.at> writes:

    mm> I don't think that I really hit the exponential wall anywhere
    mm> so it's probably just that type-checking takes much longer
    mm> than I had expected.  Well, I can live with it...

Note that it's not type-checking that's painful so much as type
reconstruction.  If it were possible to provide O'Caml with an
explicitly typed representation, simply checking the types should be
quite easy.  (Is it well typed?  Is it not well typed?)  Type
reconstruction, on the other hand, requires term unification and the
like, and takes a bit more effort.

How hard would it be (probably difficult) to expose an explicitly
typed layer from the system for automatic code generators?

John.
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Turning off type-checking

[Jacques Garrigue]

From: John Prevost <visigoth@cs.cmu.edu>
> >>>>> "mm" == Markus Mottl <markus@oefai.at> writes:
> 
>     mm> I don't think that I really hit the exponential wall anywhere
>     mm> so it's probably just that type-checking takes much longer
>     mm> than I had expected.  Well, I can live with it...
> 
> Note that it's not type-checking that's painful so much as type
> reconstruction.  If it were possible to provide O'Caml with an
> explicitly typed representation, simply checking the types should be
> quite easy.  (Is it well typed?  Is it not well typed?)  Type
> reconstruction, on the other hand, requires term unification and the
> like, and takes a bit more effort.

That's not so clear. Unification in itself is not very expensive, not
necessarily more than matching.
Things only become slow when types are big, and this would be the same
in a language without type reconstruction. The fact is that you get
much more easily big types in ocaml, just because you don't have to
write them :-) and also because lots of type equalities are by
structure.
Yet, I believe that ocamlc is faster than most java compilers, and java
doesn't have type reconstruction.

> How hard would it be (probably difficult) to expose an explicitly
> typed layer from the system for automatic code generators?

This would be easy, but dangerous. And you would have to do your own
type inference anyway, to put the proper types on the nodes, so I'm
not sure you would gain anything.
If you want to try, the code is in driver/compile.ml.
Just get rid of the beginning of Compile.implementation: Pparse.file and
Typemod.type_implementation. For efficiency you probably want to build
your tree with another program, dump it with output_value, and recover
it here with input_value. If all internal types are very simple, this
may be efficient.

    Jacques
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Turning off type-checking

[John Max Skaller]

Jacques Garrigue wrote:

>>
>>It would be really nice if there were some command-line flag for the
>>OCaml-compilers which turns off every check that is not required under the
>>assumption that the given OCaml-code is (type) correct as is guaranteed in
>>my case. Would this be easily possible? What else could I do to reduce the
>>amount of work the OCaml-compiler has to do? Insert Obj.magic everywhere?
>>
>One thing you might want to try is to write your own interpreter for
>your subset of ocaml. 
>
Heh. Or just use Felix! Felix doesn't do
Hindley-Milner type inference, so the problem should go away.
It does a restricted form of type deduction (bottom up only ..)

    http://felix.sourceforge.net

Here is the output and your model encoded as Felix script.
Your code generator only needs tiny tweaks to make it generate
Felix.

--- run the script below ------
[skaller@pelican] ~/links/flx>./bin/flx --test ttt
TESTMODE: running felix from current directory
Very Very High



--- ttt.flx ------------------------
#include <std.flx>
union  satisfaction = | Low | High | Very of satisfaction;
union  diameter = | Large | Small;
union  sort = | Mozzarella | Gorgonzola;
union topping = | Cheese of sort | Tomatoes | Mushrooms;
union  spiced = | False | True;
union  meal =
    | WienerSchnitzel of diameter
    | Pizza of (diameter * spiced * topping)
    | TapirSoup of spiced;

fun model (meal_d1:meal):satisfaction =
  let satisfaction_c1 =
    match meal_d1 with
    | TapirSoup ?spiced_d1 =>
      match spiced_d1 with
        | True => Low
        | False => High
      endmatch
    | Pizza (_, ?spiced_d1, ?topping_d1) =>
        let satisfaction_c1 =
          match spiced_d1 with
          | True =>
          match topping_d1 with
        | Cheese ?sort_d1 =>
          match sort_d1 with
          | Gorgonzola => Low
          | Mozzarella => High
          endmatch
          | _ => High
          endmatch
          | False => Low
          endmatch
        in
        Very satisfaction_c1
    | WienerSchnitzel _ => Low
    endmatch
    in
  Very satisfaction_c1
;

fun string_of(x:satisfaction)=
  match x with
  | Low => "Low"
  | High => "High"
  | Very ?z => "Very " + string_of z
  endmatch
;

val MyMeal = Pizza (Large,True, Cheese Mozzarella);
print (string_of (model MyMeal)); endl;

-- 
John Max Skaller, mailto:skaller@ozemail.com.au
snail:10/1 Toxteth Rd, Glebe, NSW 2037, Australia.
voice:61-2-9660-0850




-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Turning off type-checking

[Markus Mottl]

On Thu, 16 May 2002, John Max Skaller wrote:
> Hmm. The standard programmers trick here is to lift out the
> nested components, at the cost of passing the environment as
> arguments: if you type the arguments, it short circuits inference.

This would make models much less readable: there may be hundreds of
variables! Not much fun to pass all this around...

> BTW: you can encode the "Very" recursion as an integer.  For some
> models .. eg the model is a grammar and the data is a program with
> output a parse tree .. this optimisation isn't useful .. but in the
> 'real' world a lot of data is scalar rather than recursive.

This would not gain much: recursion is mostly there for convenient
specification. In most cases the user will provide types of finite
cardinality only.

Regards,
Markus Mottl

-- 
Markus Mottl                                             markus@oefai.at
Austrian Research Institute
for Artificial Intelligence                  http://www.oefai.at/~markus
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Turning off type-checking

[John Max Skaller]

Markus Mottl wrote:

>
>---------------------------------------------------------------------------
>let model meal_d1 =
>  let satisfaction_c1 =
>    (match meal_d1 with
>    | TapirSoup spiced_d1 ->
>        (match spiced_d1 with
>        | True -> Low
>        | False -> High)
>    | Pizza (_, spiced_d1, topping_d1) ->
>        let satisfaction_c1 =
>          (match spiced_d1 with
>          | True ->
>              (match topping_d1 with
>              | Cheese sort_d1 ->
>                  (match sort_d1 with
>                  | Gorgonzola -> Low
>                  | Mozzarella -> High)
>              | _ -> High)
>          | False -> Low) in
>        Very satisfaction_c1
>    | WienerSchnitzel _ -> Low) in
>  Very satisfaction_c1
>---------------------------------------------------------------------------
>
>If there are, say, mappings from 100 to 100 variables and thousands of
>deeply structured sample values (a "real-world" problem), the models
>can look quite terrifying.
>

Hmm. The standard programmers trick here is to lift out the
nested components, at the cost of passing the environment as
arguments: if you type the arguments, it short circuits inference.

BTW: you can encode the "Very" recursion as an integer.
For some models .. eg the model is a grammar and the
data is a program with output a parse tree .. this optimisation
isn't useful .. but in the 'real' world a lot of data is scalar
rather than recursive.


-- 
John Max Skaller, mailto:skaller@ozemail.com.au
snail:10/1 Toxteth Rd, Glebe, NSW 2037, Australia.
voice:61-2-9660-0850




-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Turning off type-checking

[malc]

On Tue, 14 May 2002, Oliver Bandel wrote:

> On Tue, 14 May 2002, Francois Pottier wrote:
> 
> [...]
> > O'Caml's type inference algorithm is sub-optimal for at least one
> > reason: it performs the occurs check at every unification step,
> > instead of delaying it until the current `let' binding is exited.
> 
> Would it help to use the Lazy-module and rewrite some parts
> od the application that uses so much time, if written "unlazy"?
> 
> BTW: When (in which kind of application) does the Lazy-module
>      really helps increasing performance?

The compiler itself uses Lazy in environment manager (typing/env.ml)
Xavier et al can probably shed more light on benefits.

-- 
mailto:malc@pulsesoft.com

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Turning off type-checking

[Oliver Bandel]

On Tue, 14 May 2002, Francois Pottier wrote:

[...]
> O'Caml's type inference algorithm is sub-optimal for at least one
> reason: it performs the occurs check at every unification step,
> instead of delaying it until the current `let' binding is exited.

Would it help to use the Lazy-module and rewrite some parts
od the application that uses so much time, if written "unlazy"?

BTW: When (in which kind of application) does the Lazy-module
     really helps increasing performance?

Ciao,
   Oliver

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Turning off type-checking

[Markus Mottl]

On Tue, 14 May 2002, Francois Pottier wrote:
> The worst-case complexity is obtained by nesting `let' bindings
> on the left side, i.e.
> 
>   let x1 = let x2 = let x3 = ...
> 
> Do you generate such code, Markus?

There may indeed be many cases of nested "let"s and also pattern-matches.

Just to give an example of how this works, given this data specification
(usual algebraic datatypes) + data samples (mappings from one domain
to another):

---------------------------------------------------------------------------
SPEC MySpec = BEGIN
  satisfaction = Low | High | Very satisfaction.
  diameter = Large | Small.
  sort = Mozzarella | Gorgonzola.
  topping = Cheese sort | Tomatoes | Mushrooms.
  spiced = False | True.
  meal =
    | WienerSchnitzel diameter
    | Pizza (diameter * spiced * topping)
    | TapirSoup spiced.
END

DATA MyData : (meal : MySpec) -> (satisfaction : MySpec) = BEGIN
  Pizza (Large, True, Cheese Mozzarella) -> Very (Very High).
  Pizza (Large, True, Cheese Gorgonzola) -> Very (Very Low).
  Pizza (Large, False, Tomatoes) -> Very (Very Low).
  WienerSchnitzel Small -> Very Low.
  TapirSoup True -> Very Low.
  TapirSoup False -> Very High.
END
---------------------------------------------------------------------------

The generated code (induced function) would look like this:

---------------------------------------------------------------------------
let model meal_d1 =
  let satisfaction_c1 =
    (match meal_d1 with
    | TapirSoup spiced_d1 ->
        (match spiced_d1 with
        | True -> Low
        | False -> High)
    | Pizza (_, spiced_d1, topping_d1) ->
        let satisfaction_c1 =
          (match spiced_d1 with
          | True ->
              (match topping_d1 with
              | Cheese sort_d1 ->
                  (match sort_d1 with
                  | Gorgonzola -> Low
                  | Mozzarella -> High)
              | _ -> High)
          | False -> Low) in
        Very satisfaction_c1
    | WienerSchnitzel _ -> Low) in
  Very satisfaction_c1
---------------------------------------------------------------------------

If there are, say, mappings from 100 to 100 variables and thousands of
deeply structured sample values (a "real-world" problem), the models
can look quite terrifying.

In another still comparatively small test case with 1000 random samples
the generated code requires about 1.6MB. What concerns me here is that
the OCaml-interpreter requires more than 60MB to check it!

> Markus, do the sub-expressions in your programs have huge types?

Well, depends on the notion of "huge". It can happen that the model
factors out redundant data constructors from large structures. Then it
has to pack and unpack somewhat large tuples, e.g.:

  let (v7_c1, (* snip 13 bindings *) v7_c15) =
    (match v6_d1 with
    ...) in
  (v7_c1, V7S (V6A, v6_c2), ...)

But the size of the types is probably not the real issue, because it is
still strongly tied to the data. The structure of the data surely plays
a role, but its size puts a limit on the size of the types.

On Tue, 14 May 2002, Alain Frisch wrote:
> It seems that what takes time is occurence checking (disabled with
> -rectypes) and pretty-printing of types (because internally, there are
> many sharings), not type inference itself. For this (unatural) example,
> bad behaviour of occurence checking is visible (less than 0.04 seconds
> with -rectypes, and more than 10 minutes [I'm not patient enough to
> wait more] without -rectypes).

I am afraid, but this does not change much, the timing difference is
lower than 10%. Maybe I am just asking for too much, and it is the sheer
size of the code that doesn't allow more efficiency?

Anyway, as it seems, parsing medium-sized test cases takes about an
order of magnitude less time than the subsequent type checking so there
may be points for improvement...

Regards,
Markus

-- 
Markus Mottl                                             markus@oefai.at
Austrian Research Institute
for Artificial Intelligence                  http://www.oefai.at/~markus
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Turning off type-checking

[Christophe Raffalli]

Le mar 14/05/2002 à 10:20, Alain Frisch a écrit :
 
> Mmm, I thought (misleaded by a teacher, of course) that the following
> would exhibit exponential behavior of type-inference:
> 
> let f y z = (z y) y
> let f y = f (f y)
> let f y = f (f y)
> let f y = f (f y)
> let f y = f (f y)
> let f y = f (f y)
> (* ad libitum *)
> 
> It seems that what takes time is occurence checking (disabled
> with -rectypes) and pretty-printing of types (because internally, there

For pretty printing, why not printing types with sharing like

val f : type 'b = 'a -> 'a in 'b -> 'b.

For large type it can be easier to read (especially if you could choose
the name of type variables):

# let f x:'c = x;;
val f : 'a -> 'a = <fun>

Is very ennoying and should really be

# let f x:'arg = x;;
val f : 'arg -> 'arg = <fun>

-- 
Christophe Raffalli
Université de Savoie
Batiment Le Chablais, bureau 21
73376 Le Bourget-du-Lac Cedex

tél: (33) 4 79 75 81 03
fax: (33) 4 79 75 87 42
mail: Christophe.Raffalli@univ-savoie.fr
www: http://www.lama.univ-savoie.fr/~RAFFALLI
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Turning off type-checking

[Alain Frisch]

On Tue, 14 May 2002, Francois Pottier wrote:

> The worst-case complexity is obtained by nesting `let' bindings
> on the left side, i.e.
>
>   let x1 = let x2 = let x3 = ...
>
> Do you generate such code, Markus?

Mmm, I thought (misleaded by a teacher, of course) that the following
would exhibit exponential behavior of type-inference:

let f y z = (z y) y
let f y = f (f y)
let f y = f (f y)
let f y = f (f y)
let f y = f (f y)
let f y = f (f y)
(* ad libitum *)

It seems that what takes time is occurence checking (disabled
with -rectypes) and pretty-printing of types (because internally, there
are many sharings), not type inference itself. For this (unatural)
example, bad behaviour of occurence checking is visible
(less than 0.04 seconds with -rectypes, and more than 10 minutes
[I'm not patient enough to wait more] without -rectypes).


-- Alain

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Turning off type-checking

[eijiro_sumii]

From: Francois Pottier <francois.pottier@inria.fr>
> > Well, type-checking ML involves more than term unification -- the 
> > worst case complexity is something truly horrible (EXP-time).
> > Having said this, for most programs, the worst-case complexity
> > rarely, if ever arises in "natural" code.  (I've not run into
> > it...)
> 
> The worst-case complexity is obtained by nesting `let' bindings
> on the left side, i.e.
> 
>   let x1 = let x2 = let x3 = ...
> 
> Do you generate such code, Markus?

Just for information, I once came across a real situation where I
generated similar code with too much nested 'let' and
ocamlc/ocamlopt/ocamlc.opt/ocamlopt.opt ran out of memory or did not
terminate within a practical amount of time.  I am not sure whether
that was because of type checking, though.  (See the "PLClubCN"
version of our entry to ICFP Programming Contest 2000 in case of any
interest...)

--
Eijiro Sumii (http://www.yl.is.s.u-tokyo.ac.jp/~sumii/)
Research Associate, Department of Computer Science, University of Tokyo
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Turning off type-checking

[Francois Pottier]

> Well, type-checking ML involves more than term unification -- the 
> worst case complexity is something truly horrible (EXP-time).
> Having said this, for most programs, the worst-case complexity
> rarely, if ever arises in "natural" code.  (I've not run into
> it...)

The worst-case complexity is obtained by nesting `let' bindings
on the left side, i.e.

  let x1 = let x2 = let x3 = ...

Do you generate such code, Markus?

> So, I'd actually be surprised if there was any significant speedup
> obtained by eliminating the type-inference from the compilation
> path.  

O'Caml's type inference algorithm is sub-optimal for at least one
reason: it performs the occurs check at every unification step,
instead of delaying it until the current `let' binding is exited.
This causes it to have (theoretical) quadratic complexity, instead
of linear, in the case where `let' bindings aren't left-nested.
However, in practice, this has never turned out to be a problem.
Markus, do the sub-expressions in your programs have huge types?

-- 
François Pottier
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

RE: [Caml-list] Turning off type-checking

[Gregory Morrisett]

> Could the type experts on this list confirm or deny that :
> 	- For ``classical'' types, type-checking amounts to 
> term unification.
> 	- Term unification can be done in worst-case linear-time.
> 	- Ocaml's unification algorithm is worst-case suboptimal.
> 	- This explains the ``awful amount of time'' needed for 
> type checking.

Well, type-checking ML involves more than term unification -- the 
worst case complexity is something truly horrible (EXP-time).
Having said this, for most programs, the worst-case complexity
rarely, if ever arises in "natural" code.  (I've not run into
it...)

So, I'd actually be surprised if there was any significant speedup
obtained by eliminating the type-inference from the compilation
path.  

-Greg
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners