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 p8R8YE9F003930 for ; Tue, 27 Sep 2011 10:34:14 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AlsBAByKgU7D3XqWmWdsb2JhbABBFoRNlByOfRQBAQEBAQgLCwcUJoFTAQEEASMEERElEAsLEAgCAgkIFQICHwIkEgYTEgmHXQIEpxqSEYEsgWxcggYxYASMB4dLhSKEdoce X-IronPort-AV: E=Sophos;i="4.68,448,1312149600"; d="scan'208";a="121646294" Received: from ubpmes.univ-bpclermont.fr ([195.221.122.150]) by mail1-smtp-roc.national.inria.fr with ESMTP; 27 Sep 2011 10:34:09 +0200 Received: from localhost (localhost.localdomain [127.0.0.1]) by ubpmes.univ-bpclermont.fr (Postfix) with ESMTP id 58708762207 for ; Tue, 27 Sep 2011 10:34:09 +0200 (CEST) X-Virus-Scanned: amavisd-new at univ-bpclermont.fr Received: from ubpmes.univ-bpclermont.fr ([127.0.0.1]) by localhost (ubpmes.univ-bpclermont.fr [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id UlvomzNaYGMV for ; Tue, 27 Sep 2011 10:34:04 +0200 (CEST) Received: from [172.27.1.69] (unknown [193.54.50.250]) by ubpmes.univ-bpclermont.fr (Postfix) with ESMTP id 94EB6761A88 for ; Tue, 27 Sep 2011 10:34:04 +0200 (CEST) Message-Id: From: =?ISO-8859-1?Q?Jocelyn_S=E9rot?= To: OCaML Mailing List In-Reply-To: <4E80E9F4.4050507@univ-savoie.fr> Content-Type: text/plain; charset=UTF-8; format=flowed; delsp=yes Mime-Version: 1.0 (Apple Message framework v935.3) Date: Tue, 27 Sep 2011 10:34:04 +0200 References: <10F5DBD5-5387-408C-967B-50B37367A6E1@lasmea.univ-bpclermont.fr> <4E806C6F.5050407@gmail.com> <4FAB50A9-43BE-402D-8420-524573F10668@lasmea.univ-bpclermont.fr> <4E80E9F4.4050507@univ-savoie.fr> X-Mailer: Apple Mail (2.935.3) Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id p8R8YE9F003930 X-Validation-by: jocelyn.serot@ubpmes.univ-bpclermont.fr Subject: Re: [Caml-list] Dependent types ? You're perfectly right Christophe, I now realize that i've opened some kind of Pandora box. Supporting function declaration > concat : int -> int -> int (or multiplication) would be great (even with only addition on sizes), but a too long term goal for me (esp. taking into account that i'm by no means a specialist in type theory !). So, a simple approximation like add : int -> int -> int (in which the size considerations are supposed to be handled at the VHDL level) would be anough for me.. Jocelyn Le 26 sept. 11 à 23:09, Christophe Raffalli a écrit : > Hello, > > Le 26/09/11 18:44, Gabriel Scherer a écrit : >>> Phantom types could be a solution but we must declare a new type for >>> each possible size, which is cumbersome / annoying. >> If you define the type system yourself, you can easily add a family >> of >> type constants `size` (with `n` an integer literal) to the default >> environment of the type checker. Then you can define a parametrized >> type `type 's sized_int` (or float, etc.) and instantiate it with any >> of the size. > Another issue is if you wand function additionning size like > > concat : int -> int -> int (or multiplication) > > and zext : int -> int (when m > n) > > Then your type system is likely to have to solve problems in > Pressburger > arithmetics. > Even only with existential quantifications, this is still not trivial > (no elimination of quantifiers). > > But you could probably reuse the code of the Coq Omega tactics ... Or > some other library > like Facile, if you accept limited ranges for you sizes. > > I always wanted something like that for size of arrays in OCaml ... > > If you have no addition, then this is much easier... and if you have > multiplication, this is likely to be undecidable > (diophantian equations ...). > > So you should first list the functions you want with their types ... > > Regards, > Christophe > > Which is decidable, but not trivial ... > > > >> >> One issue with this minimal -- in term of modifications -- mechanism >> is that you can represent meaningless types such as `float >> size_int` : >> `float` is not a size. The canonical way to handle this is to add >> a kind system on top of your type system, that would classify the >> types into different kinds. Usual types would have kind `★`, and >> sizes >> would have kind `Size`. You would then restrict the `'a` type >> variable in >> `sized_int` to be of kind `Size`: >> >> type ('a : Size) sized_int >> >> http://en.wikipedia.org/wiki/Kind_(type_theory) >> >> Remark: There is another useful way to combine kinds and sizes, which >> is to use "sized kinds" to classify types whose memory representation >> has a given size in your implementation. For example you would have >> a kind `★` for types of one machine word, `★2` for two machine >> words... This allows to keep parametric polymorphism in presence of >> non-uniform representations, but it is restricted, less general, as >> a given polymorphic definition would not quantify over all types, but >> on all types of a given kind – unless you introduce kind >> polymorphism, >> etc. It may be useful for typing low-level programs, but it doesn't >> look like what you're looking for here. >> >> >> On Mon, Sep 26, 2011 at 5:55 PM, Jocelyn Sérot >> wrote: >>> Thanks to all for your answers. >>> Phantom types could be a solution but we must declare a new type >>> for each >>> possible size, which is cumbersome / annoying. >>> Moreover, since i'm writing a DSL, the fact that they do not >>> require a >>> modification to the existing type system is not really an advantage. >>> My language has its own type system (largely inspired from >>> OCaml's) so what >>> I was looking for was more a way to modify the type representation >>> to >>> support the requested behavior. >>> To those familiar with Caml compiler source code, i was wondering >>> if i could >>> hack the following definitions (from types. ml) >>> type typ = >>> | TyVar of typ_var >>> | TyTerm of string * typ list >>> and typ_var = >>> { mutable level: int; >>> mutable value: tyvar_value } >>> and tyvar_value = >>> | Unknown >>> | Known of typ >>> by adding a notion of "size variable" (sorry if this sounds >>> imprecise, this >>> is still a but hazy in my mind..) >>> type typ = >>> | TyVar of typ_var >>> | TyTerm of string * typ list * typ_size >>> and typ_sz = >>> { mutable value: tysz_value } >>> and tyvar_value = >>> | Unknown >>> | Known of int >>> and update the unification engine accordingly.. >>> Well, the easiest answer is maybe just to try :-S >>> I'm just a bit surprised that no one seems to have proposed such an >>> extension yet. >>> Jocelyn >>> Le 26 sept. 11 à 14:45, Yaron Minsky a écrit : >>> >>> As written, the behavior of the types might not be what you >>> expect, since >>> addition of two 16 bit ints may result in an int that requires 17 >>> bits. >>> >>> When using phantom types, you need to be especially careful that >>> the types >>> mean what you think they mean. >>> >>> On Sep 26, 2011 8:13 AM, "Denis Berthod" >>> wrote: >>>> Hello, >>>> >>>> I think that achieving something very near from what you whant is >>>> relatively easy using phantom types. >>>> That avoid the boxing/unboxing in records. >>>> >>>> type i16 >>>> type i32 >>>> >>>> module SizedInt: >>>> sig >>>> type 'a integer >>>> val int16: int -> i16 integer >>>> val int32: int -> i32 integer >>>> val add: 'a integer -> 'a integer -> 'a integer >>>> end >>>> = >>>> struct >>>> type 'a integer = int >>>> >>>> let int16 x = x >>>> let int32 x = x >>>> >>>> let add x y = x + y >>>> end >>>> >>>> then >>>> >>>> open SizedInt >>>> >>>> let bar = >>>> let x = int16 42 in >>>> foo x >>>> >>>> must have type i16 integer -> i16 integer >>>> >>>> Regards, >>>> >>>> Denis Berthod >>>> >>>> >>>> Le 26/09/2011 13:42, Jocelyn Sérot a écrit : >>>>> Hello, >>>>> >>>>> I've recently come across a problem while writing a domain >>>>> specific >>>>> language for hardware synthesis >>>>> (http://wwwlasmea.univ-bpclermont.fr/Personnel/Jocelyn.Serot/caph.html >>>>> ). >>>>> The idea is to extend the type system to accept "size" >>>>> annotations for >>>>> int types (it could equally apply to floats). >>>>> The target language (VHDL in this case) accept "generic" >>>>> functions, >>>>> operating on ints with variable bit width and I'd like to >>>>> reflect this >>>>> in the source language. >>>>> >>>>> For instance, I'd like to be able to declare : >>>>> >>>>> val foo : int * int -> int >>>>> >>>>> (where the type int is not annotated, i.e. "generic") >>>>> >>>>> so that, when applied to, let say : >>>>> >>>>> val x : int<16> >>>>> val y : int<16> >>>>> >>>>> (where <16> is a size annotation), >>>>> >>>>> like in >>>>> >>>>> let z = foo (x,y) >>>>> >>>>> then the compiler will infer type int<16> for z >>>>> >>>>> In fact, the exact type signature for foo would be : >>>>> >>>>> val foo : int * int -> int >>>>> >>>>> where "s" would be a "size variable" (playing a role similar to >>>>> a type >>>>> variable in, for ex : val map : 'a list -> ('a ->'b) -> 'b list). >>>>> >>>>> In a sense, it has to do with the theory of sized types (Hughes >>>>> and >>>>> Paretto, .. ) and dependent types (DML for ex), but my goal is far >>>>> less ambitious. >>>>> In particular, i dont want to do _computations_ (1) on the size >>>>> (and, >>>>> a fortiori, don't want to prove anything on the programs). >>>>> So sized types / dependent types seems a big machinery for a >>>>> relatively small goal. >>>>> My intuition is that this is just a variant of polymorphism in >>>>> which >>>>> the variables ranged over are not types but integers. >>>>> Before testing this intuition by trying to implement it, I'd >>>>> like to >>>>> know s/o has already tackled this problem. >>>>> Any pointer - including "well, this is trivial" ! ;-) - will be >>>>> appreciated. >>>>> >>>>> Best wishes >>>>> >>>>> Jocelyn >>>>> >>>>> (1) i.e. i dont bother supporting declarations like : val mul : >>>>> int >>>>> * int -> int <2*n> ... >>>>> >>>>> >>>>> >>>> >>>> -- >>>> Caml-list mailing list. Subscription management and archives: >>>> https://sympa-roc.inria.fr/wws/info/caml-list >>>> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners >>>> Bug reports: http://caml.inria.fr/bin/caml-bugs >>>> >>> >> > > > -- > 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 > --------------------------------------------- > >