Re: fancy types (was Re: [Caml-list] ocaml killer)

[Thomas Fischbacher <Thomas.Fischbacher@Physik.Uni-Muenchen.DE>]

On Thu, 29 Jan 2004, William Lovas wrote:

> I've passed functions to themselves before without ever having to make use
> of such a function

Look here:

# let fac n = let do_rec specialist n = if n = 0 then 1 else n * specialist specialist (n-1) in do_rec do_rec n;;

Characters 74-84:
  let fac n = let do_rec specialist n = if n = 0 then 1 else n * 
specialist specialist (n-1) in do_rec do_rec n;;
                                                                            
^^^^^^^^^^
This expression has type 'a -> 'b -> 'c but is here used with type 'a

# let fac n = let do_rec specialist n = if n = 0 then 1 else n * (Obj.magic specialist) specialist (n-1) in do_rec do_rec n;;
val fac : int -> int = <fun>

# fac 8;;
- : int = 40320

This is just one stupid example where the type system gets in the way 
while it should not. Yes, here it does not make too much sense, as I 
would use let rec if I wanted to just create a factorial, but it shows 
the general principle: whenever I have a function that handles a "base 
case" and takes a specialist to pass the recursive case on to, which may 
in turn again require a specialist, I cannot give the specialist itself as 
further specialist, "because unification would give infinite type", as 
other functional languages with similar type system (Haskell or SML, say),
like to put it. and there are quite some cases where one would like to 
employ such techniques. (In Common LISP, I use it regularly when working 
with the "screamer" nondeterministic evaluation module: screamer's biggest 
advantage is that it is readily available, but it is conceptually broken 
at many levels. As it in particular cannot code walk a LABELS, I have to 
resort to such techniques for manual resolution of fixed points to make 
recursive nondeterministic functions...)

As one particular consequence, I also cannot easily map some combinators 
to ocaml:

# let l_combinator x y = x (y y);;

Characters 28-29:
  let l_combinator x y = x (y y);;
                              ^
This expression has type 'a -> 'b but is here used with type 'a

But there are more issues... Look here:

# type ('a,'b) mypair = Nil | Cons of 'a * 'b;;
type ('a, 'b) mypair = Nil | Cons of 'a * 'b


Try defining something like this on it:


# let rec my_len x = match x with | Nil -> 0 | (Cons (p,q)) -> 1+my_len q;;

Characters 70-71:
  let rec my_len x = match x with | Nil -> 0 | (Cons (p,q)) -> 1+my_len q;;
                                                                        ^
This expression has type 'a but is here used with type ('b, 'a) mypair


OF COURSE opinions may differ whether this is really a problem or not. 
Certainly, you can implement every algorithm you want in ocaml, but I 
personally feel that a Hindley-Milner like type system restricts my 
freedom too much and occasionally gets in the way when I want to implement
solutions to problems that are most naturally viewed from a lambda 
calculus point of view. On the other hand, I experience the benefits of 
such a type system as limited; it is able to catch a lot of mistakes I 
would not have made anyway. Nah, I'm rather a LISP hacker.

> (which already exists in the standard library, it being
> mysteriously named Obj.magic and its use being highly discouraged).

For good. I bet this feature exists precisely to keep the LISP wizards 
happy who know about and are not afraid of these dark corners, and have 
(maybe out of stubbornness :-) ) a strong desire writing LISP code in 
ocaml. If there were only honest and upright ocaml programmers, such a 
feature certainly wouuld not exist, and hence it is perhaps a good idea to 
strongly discourage its use.

[I still do not have a good overview over the ocaml library and thus did 
not know this function. Thanks for that piece of information.]


BTW: I also strongly assume that internally, ocaml uses type tagging 
anyway, at least for the garbage collector; hence it may be possible to 
use just the engine of ocaml and build a dynamically typed lisp on top of 
it...? Would be terrific...


-- 
regards,               tf@cip.physik.uni-muenchen.de                 (o_
Dr. Thomas Fischbacher -  http://www.cip.physik.uni-muenchen.de/~tf  //\
(lambda (n) ((lambda (p q r) (p p q r)) (lambda (g x y)              V_/_
(if (= x 0) y (g g (- x 1) (* x y)))) n 1))                     (Debian GNU)

-------------------
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