Re: [Caml-list] cyclic types

[Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr>]

[-- Attachment #1: Type: text/plain, Size: 3501 bytes --]


> 
>       let f x = x :: x
> 
> where the author of that code really intended
> 
>       let f x = x @ x
> 
> With -rectypes, the wrong definition (with ::) is accepted with type
> 
> val f : ('a list as 'a) -> 'a list = <fun>
> 
> and it's only when you try to apply f to a "normal" list that the
> problem arises, with a hard-to-understand error message:
> 
> f [1;2;3];;
>    ^
> This expression has type int but is here used with type 'a list as 'a
> 

Why do you think 'a list as 'a is an <<"impossible" recursive types>> ?
It is a very nice representation of ordinals up to epsilon_0 (curious, 
see the code below)

Why not this restriction: accept a recursive type 't as 'a only if
access to 'a in t needs to expand a definition. I mean, the cyclicity 
check at the end of unification could check that one traverses 
definition. I am not sure how OCaml treat type annotation, this will 
work only if the compiler does its best to use all type annotation.

'a list as 'a is illegal

and let f x = x @ x is illegal

type ord = ord list is legal (all type definition should be legal)

let f (x:ord) = x @ x is legal

code for curious:
--------------------------8<----------------
(* need -rectypes *)

(*
   a very short representation of ordinals up to epsilon_0 as a fixpoint 
of list
*)
type ord = ord list


(* comparison: you must normalize ordinal before comparison *)
let rec compare  (o1:ord) (o2:ord) = match o1, o2 with
   | [], [] -> 0
   | [], _ -> -1
   | _, [] -> 1
   | x::o1', y::o2' ->
       match compare x y with
	-1 -> compare o1' o2
       | 1 -> compare o1 o2'
       | 0 -> compare o1' o2'

let lesseq o1 o2 = compare o1 o2 <= 0

(* compute the normal form of an ordinal*)
let rec normalize (o1:ord) =
   List.sort (fun x y -> compare y x) (List.map normalize o1)

let zero = ([] : ord)
let un = ([[]] : ord)
let deux = ([[];[]] : ord)
let omega = ([[[]]] : ord)
let deux_omega = ([[[]];[[]]] : ord)
let omega_square = ([[[];[]]] : ord)
let omega_to_the_omega = ([[[[]]]] : ord)

let addition (o1:ord) (o2:ord) = o1 @ o2

let rec multiplication (o1:ord) (o2:ord) = match o1, o2 with
   [], _ -> [] (* zero * o2 = zero *)
| _, [] -> [] (* o1 * zero = zero *)
| ([]::o1'), _ -> (* (1 + o1') * o2 = o2 + o1' * o2 *)
   addition o2 (multiplication o1' o2)
| _, ([]::o2') -> (* o1 * (1 + o2') = o1 + o1 * o2' *)
   addition o1 (multiplication o1 o2')
| (o1''::o1'),(o2''::o2') ->
     (* (w^o1'' + o1')*(w^o2'' + o2') = w^(o1''+o2'') + o2'*w^o1'' +
             o1'*w^o2'' + o1'*o2' *)
     (addition o1'' o2'')::(multiplication [o1''] o2')@
     (multiplication o1' [o2''])@(multiplication o1' o2')

(* test *)
let _ = compare [[]] [[];[]]
let _ = compare [[[]];[]] [[];[[]]]
let _ = compare [[[]]] [[];[[]]]
let _ = compare omega_to_the_omega omega_square
let _ = normalize [[];[[]]]
let _ = normalize [[[];[]];[];[[]]]
let quatre = multiplication deux deux
let quatre_omega = multiplication omega quatre
let big = normalize (multiplication omega_to_the_omega quatre_omega)


-- 
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
---------------------------------------------
IMPORTANT: this mail is signed using PGP/MIME
At least Enigmail/Mozilla, mutt or evolution
can check this signature. The public key is
stored on www.keyserver.net
---------------------------------------------

[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 252 bytes --]