Re: [Caml-list] Depend-type beginner question

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

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

Vincent Aravantinos a écrit :
> 
> Le 5 oct. 07 à 17:41, Christopher L Conway a écrit :
> 
>> On 10/5/07, Vincent Aravantinos <vincent.aravantinos@gmail.com> 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
---------------------------------------------


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