Version française
Home     About     Download     Resources     Contact us    
Browse thread
Depend-type beginner question
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Vincent Aravantinos <vincent.aravantinos@g...>
Subject: Re: [Caml-list] Depend-type beginner question

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