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: Lukasz Stafiniak <lukstafi@g...>
Subject: Re: [Caml-list] Depend-type beginner question
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.