recursive datatypes

recursive datatypes

[Simon Helsen]

Why does Caml type-check the following program? It wouldn't in Standard ML
and I don't see the use for it, as it may lead to infinite programs...

(I don't have a french keyboard)

Pourquoi est le programme ci-desous bon type ? C'est ne pas le
cas en Standard ML et je ne comprend pas l'usage pour ca parce que le
programme peut eventuellement cours a l'infini... 

type 'a tree = Tree of 'a

let f x = Tree (f x)

----------------------- Simon Helsen ------------------------ 
--       Wilhelm-Schickard-Institut fuer Informatik        --
--           Arbeitsbereich Programmierung (PU)            --
--            Universitaet Tuebingen, Germany              --
-------------------------------------------------------------
-- http://www-pu.informatik.uni-tuebingen.de/users/helsen/ --

Re: recursive datatypes

[Xavier Leroy]

> Why does Caml type-check the following program? It wouldn't in Standard ML
> and I don't see the use for it, as it may lead to infinite programs...
> type 'a tree = Tree of 'a
> let f x = Tree (f x)

Objective Caml supports recursive types (i.e. type expressions with
cycles) because the object types need them, in particular in
situations involving binary methods.

The simplest implementation is to allow recursion in types almost
anywhere.  That's what the current 1.05 release of OCaml does.

The main drawback with this is that a number of programming errors
result in programs being well-typed with weird recursive types,
instead of being rejected by the type system as in a normal (no
recursive types) type system.  (BTW, the argument with "infinite
programs" doesn't hold, as there is nothing you can do with recursive
types that you can't do with datatypes, including embeddings of the
untyped lambda-calculus.)

For this reason, the next release of OCaml will restrict recursive
types in such a way that the recursion must go through an object type.
That should match everyone's intuitive expectations about the type
system, though it probably rules out a few cool examples.

- Xavier Leroy

Re: recursive datatypes

[Michel Quercia]

Simon Helsen wrote:

> Why does Caml type-check the following program? It wouldn't in Standard ML
> and I don't see the use for it, as it may lead to infinite programs...
>
> (I don't have a french keyboard)
>
> Pourquoi est le programme ci-desous bon type ? C'est ne pas le
> cas en Standard ML et je ne comprend pas l'usage pour ca parce que le
> programme peut eventuellement cours a l'infini...
>
> type 'a tree = Tree of 'a
>
> let f x = Tree (f x)
>

Hi,

Your code does'nt typecheck with both camllight  0.73 and ocaml 1.05.

With ocaml1.05, the following code does typecheck :

----------------------------------------
        Objective Caml version 1.05

# type 'a tree = Tree of 'a;;
type 'a tree = | Tree of 'a
# let f x = Tree (f x);;
Unbound value f
# let rec f x = Tree (f x);;
val f : 'a -> ('b tree as 'b) = <fun>
# f(3);;
Out of memory during evaluation
#
---------------------------------------

I can't explain the "('b tree as 'b)", but why your post is entitled
"recursive datatypes" ?
Did you mean :

type 'a tree = Tree of 'a tree ?

This type declaration is accepted and it is possible to build 'a tree objects
:


--------------------------------------

# type 'a tree = Tree of 'a tree;;
type 'a tree = | Tree of 'a tree
# #print_depth 5;;
# let rec x = Tree(y) and y = Tree(x);;
val x : 'a tree = Tree (Tree (Tree (Tree (Tree (Tree ...)))))
val y : 'a tree = Tree (Tree (Tree (Tree (Tree (Tree ...)))))
-------------------------------------

--
Michel Quercia
Lycee Carnot  16 bd Thiers  21000 Dijon
mailto:quercia@cal.enst.fr