divergent type

divergent type

[skaller]

Sorry for asking a general typing question not specifically related
to Ocaml .. also, I don't really know how to ask the question properly
(if I did I would know the answer too).

I have a problem in Felix compiler with infinite types. For example
the type of

	fun f(x:int)=>x,f x

is 

	(int * u) as u

which cannot be represented. In Ocaml with -rectypes this is a
legitimate type:

# let rec x = 1,x;;
val x : int * 'a as 'a =
  (1,
   (1,...

which is representable because Ocaml uses boxing (intensional
polymorphism).Smly:

# let rec f x = 1, f x;;
val f : 'a -> (int * 'b as 'b) = <fun>

Felix supports type recursion through pointers, variants also
allow it because they're modelled as pointers (boxed),
and of course functions are boxed (closures).

However some type equations (recursive types) have no
solution at all:

# let rec f x = f (x,x);;    
val f : ('a * 'a as 'a) -> 'b = <fun>

The return type is divergent: Ocaml put 'b here, but
it is a 'hack' the type of the value 'returned' is unrelated to
the type of the value input. Note that this function CAN be modified
to actually return a definite value:

let rec f n x = if x <= 0 then () else f (n-1) (x,x)

is convergent. (It is dependently type-able?)

In any case there seem to be THREE kinds of type:

1. Ordinary types.
2. Finite Recursive types (eg lists)
3. Divergent types

Perhaps someone can throw a bit more light on this?

In Felix I need to detect the difference between an 
incidental recursion (a polymorphic function just happens to call
itself for an unrelated/non-recursive purpose such as mapping
a tuple: such 'recursion' always terminates because the input
term is finite), a representable recursive type (such as a list),
and an infinite expansion. And I note the distinctions are not
representation independent (since Ocaml can handle recursive
products whilst Felix cannot do so without using a pointer).

Help!

-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net