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

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

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]

Is this a 0-list or a 1-list ? do they just put an existential  
variable -> n-list ? If this is it, it seems to me that you won't be  
able to gain much information.

??

V.