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

["Lukasz Stafiniak" <lukstafi@gmail.com>]

On 10/5/07, Vincent Aravantinos <vincent.aravantinos@gmail.com> wrote:
>
> Le 5 oct. 07 à 17:41, Christopher L Conway a écrit :
> >
> > 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 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.
>
DML (or its successor ATS) is not really a dependently typed language
IIRC. It is a polymorphically typed language which can express _some_
dependency of types on values using e.g. singleton types. The upside
is that it can limit what can be expressed to a logic manageable at
compile time. The downside is that you are limited to, e.g., linear
inequalities over integers, and this forces you to lose information
e.g. by using existential quantification.