Vincent Aravantinos a écrit : > > Le 5 oct. 07 à 17:41, Christopher L Conway a écrit : > >> On 10/5/07, Vincent Aravantinos wrote: >>> why actually dependant types cannot be implemented in ocaml ? Is the >>> type checking undecidable ? Or is it for other reason (e.g. >>> arithmetic) ? I guess it's both. But could someone develop precisely ? >> >> It's not that dependent types can't be implemented in OCaml, just that >> they haven't. See, e.g., http://www.cs.bu.edu/~hwxi/DML/DML.html >> >> I suspect the OCaml development team is not inclined to add "sexier" >> types to the core language, though I can't say if there are any >> specific technical hurdles preventing it (certainly, decidability is >> an issue)... > > I can't get how the following could ever be typed at compile time: > >> if ... then [] else [a] > if b then [] else [a] has type list(if b then 0 else 1) where is the problem ? if b then 0 else 1 may or may not be simplified if you know b. The problem is that equality over such complex types in undecidable and you have to provide proofs ... -- Christophe Raffalli Universite de Savoie Batiment Le Chablais, bureau 21 73376 Le Bourget-du-Lac Cedex tel: (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 ---------------------------------------------