divergent type
 skaller
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:   (:) 
From:  skaller <skaller@u...> 
Subject:  divergent type 
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 (n1) (x,x) is convergent. (It is dependently typeable?) 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/nonrecursive 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