Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

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 <> 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.,
> 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.