Depend-type beginner question

Depend-type beginner question

[Vincent Aravantinos]

Hi,

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 ?

Would something like http://okmij.org/ftp/Computation/lightweight- 
dependent-typing.html be implementable ?

Thanx,
Vincent

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

[Christopher L Conway]

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

Regards,
Chris

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

[Vincent Aravantinos]

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.

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

[Ashish Agarwal]

[-- Attachment #1: Type: text/plain, Size: 372 bytes --]

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

The type system is not rich enough to distinguish between 0-lists' and
1-list's. It is just a list.

[-- Attachment #2: Type: text/html, Size: 486 bytes --]

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

[Vincent Aravantinos]

Le 5 oct. 07 à 18:05, Ashish Agarwal a écrit :

> > 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.
>
> The type system is not rich enough to distinguish between 0-lists'  
> and 1-list's. It is just a list.

So what is the gain ?

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

[Christophe Raffalli]

[-- Attachment #1: Type: text/plain, Size: 1659 bytes --]

Vincent Aravantinos a écrit :
> 
> 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]
> 

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




-- 
Christophe Raffalli
Universite de Savoie
Batiment Le Chablais, bureau 21
73376 Le Bourget-du-Lac Cedex

tel: (33) 4 79 75 81 03
fax: (33) 4 79 75 87 42
mail: Christophe.Raffalli@univ-savoie.fr
www: http://www.lama.univ-savoie.fr/~RAFFALLI
---------------------------------------------
IMPORTANT: this mail is signed using PGP/MIME
At least Enigmail/Mozilla, mutt or evolution
can check this signature. The public key is
stored on www.keyserver.net
---------------------------------------------


[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 252 bytes --]

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

[Vincent Aravantinos]

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

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

[Lukasz Stafiniak]

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.

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

[Arnaud Spiwack]

>
> 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... 
I'm not sure I'm quite getting what you mean here.
 In any case, dependent types mainly means that there is a bit of 
computation inside types. This raises quite a lot of issues.
 It is way preferable, for instance, that type-checking is decidable, 
which means that one can't put arbitrary computation inside types, 
moreover, it would be preferable that a type does not read or write into 
files, that would be rather annoying.
In order to get things done, there are a few approachs, languages like 
OCaml, Haskell, and such, try to build up from decidable inference to 
richer type systems and see what they can get done, this have the 
advantages of manipulating fully usable languages; languages like Coq, 
Agda, Epigram, start with dependent types as highly expressive as 
possible, and try to retrieve features bit by bit (and thus are not 
fully usable languages). (I haven't quoted DML and PML because I still 
haven't quite looked into them, thus I can't really place them :p ).

However, to get back to the list example.
Let us suppose, in Coq syntax, that we defined lists the following way :

Inductive list (A:Type) : nat -> Type :=
   | Nil : forall A, list A 0
   | Cons : forall A n, A -> list A n -> list A (S n)

These are lists that carry their length.

The program :

if b then
  []
else
  [a]

can only be typed as a *dependent* elimination of b, as Christophe said 
the type is "if b then list A 0 else list A 1". The whole point of 
dependent types is that this is a perfectly well-formed type. And it can 
be checked before compiling "if b then [] else [a]" that it actually 
have type "if b then list A 0 else list A 1". The schyzophrenia of 
dependent types, is that types depend on previously compiled (and types) 
expressions, it still is static typing, just weirder (and much more fun 
if you want my opinion ;) ).


Arnaud Spiwack