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

[Vincent Aravantinos <vincent.aravantinos@gmail.com>]

Le 5 oct. 07 à 18:18, Christophe Raffalli a écrit :

> Vincent Aravantinos a écrit :
>> 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 ...

Of course. So languages that claim to have dependant types all delay  
the type checking to compile-time or formal proof. I am reassured, I  
thought I was missing some big thing...

Thanks a lot to all,
Vincent