cyclic types
[
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:  Christophe Raffalli <Christophe.Raffalli@u...> 
Subject:  Re: [Camllist] cyclic types 
> > 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 hardtounderstand 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 BourgetduLac Cedex tél: (33) 4 79 75 81 03 fax: (33) 4 79 75 87 42 mail: Christophe.Raffalli@univsavoie.fr www: http://www.lama.univsavoie.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 