From mboxrd@z Thu Jan  1 00:00:00 1970
X-Sympa-To: caml-list@inria.fr
Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82])
	by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p8RCPa1C014868
	for <caml-list@sympa-roc.inria.fr>; Tue, 27 Sep 2011 14:25:39 +0200
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AgEBAA3AgU5QDPKFkGdsb2JhbABCqAsBAQEBCQkNBxQDI4FTAQEEAThRCy0ZVwaICwK4YYN0gjdgBKUI
X-IronPort-AV: E=Sophos;i="4.68,449,1312149600"; 
   d="scan'208";a="121700587"
Received: from smtp11.smtpout.orange.fr (HELO smtp.smtpout.orange.fr) ([80.12.242.133])
  by mail1-smtp-roc.national.inria.fr with ESMTP; 27 Sep 2011 14:25:39 +0200
Received: from new-host-3.home ([86.209.216.124])
	by mwinf5d46 with ME
	id doRe1h00H2hd8vq03oRetF; Tue, 27 Sep 2011 14:25:39 +0200
X-ME-engine: default
Message-Id: <BDFD9DA5-5684-4BFF-8484-7FD66D22EA12@wanadoo.fr>
From: =?ISO-8859-1?Q?Jocelyn_S=E9rot?= <jocelyn.serot@wanadoo.fr>
To: OCaML Mailing List <caml-list@inria.fr>
In-Reply-To: <CAMoPVjc1FmKtrrcz7n4jCGH0e4+jPgrSB-G23pB6SM-Km829mg@mail.gmail.com>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed; delsp=yes
Mime-Version: 1.0 (Apple Message framework v935.3)
Date: Tue, 27 Sep 2011 14:25:38 +0200
References: <10F5DBD5-5387-408C-967B-50B37367A6E1@lasmea.univ-bpclermont.fr> <4E806C6F.5050407@gmail.com> <CADKNfhLMqAstEUJyik4DZ9QEBdb-4D-=9HnDgy3dF0WbfrnnXg@mail.gmail.com> <4FAB50A9-43BE-402D-8420-524573F10668@lasmea.univ-bpclermont.fr> <CAPFanBFKGYj8KSh43m8BVZzMh0_Bm_h_bZOes-iUhJTBfKsZTg@mail.gmail.com> <62D492AB-ABD5-4A66-BE41-6191D5813AA5@lasmea.univ-bpclermont.fr> <CAPFanBHKHWsgPLZo7GpzWj8tjY1u4DM2V7z7DiMb+b7O57eOGA@mail.gmail.com> <CAMoPVjc1FmKtrrcz7n4jCGH0e4+jPgrSB-G23pB6SM-Km829mg@mail.gmail.com>
X-Mailer: Apple Mail (2.935.3)
Content-Transfer-Encoding: 8bit
X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id p8RCPa1C014868
X-Validation-by: jocelyn.serot@wanadoo.fr
Subject: Re: [Caml-list] Dependent types ?

Well, clever and funny idea ;-)

But not specially user-friendly, esp. if you take into account the  
fact that the user of my DSL are mainly VHDL programmers, not  
particularly familiar with FP and polymorphic type systems...

Thanks for the idea, anyway

Jocelyn

Le 27 sept. 11 à 11:41, Arnaud Spiwack a écrit :

>
> Yes, this is right. You can already experiment in ocaml, as Denis
> Berthod suggested, by adding abstract types by hand instead of having
> constants in the initial environment.
>
> You can also embed the natural numbers in Ocaml's type system by  
> declaring the following two types:
>
> type 'a s
> type z
>
> Granted 32 would be written z s s s s s s s s s s s s s s s s s s s  
> s s s s s s s s s s s s s which may or may not be considered  
> legible. But at least there is no absolute need for infinitely many  
> constants.