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 p8R8O0Dm003415 for ; Tue, 27 Sep 2011 10:24:00 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AlsBANiHgU7D3XqWmWdsb2JhbABBhGOUHI59FAEBAQEBCAsLBxQmgVMBAQQBIwQRNhsLGAICCR0CAh8CJBIGExIJh10CBKcGkg+BLIFsgmIxYASMB4dLhSKEdoce X-IronPort-AV: E=Sophos;i="4.68,448,1312149600"; d="scan'208";a="121644122" Received: from ubpmes.univ-bpclermont.fr ([195.221.122.150]) by mail1-smtp-roc.national.inria.fr with ESMTP; 27 Sep 2011 10:23:58 +0200 Received: from localhost (localhost.localdomain [127.0.0.1]) by ubpmes.univ-bpclermont.fr (Postfix) with ESMTP id E6BE37C7474 for ; Tue, 27 Sep 2011 10:23:57 +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 yxX6nPFRg509 for ; Tue, 27 Sep 2011 10:23:56 +0200 (CEST) Received: from [172.27.1.69] (unknown [193.54.50.250]) by ubpmes.univ-bpclermont.fr (Postfix) with ESMTP id 723097C714E for ; Tue, 27 Sep 2011 10:23:56 +0200 (CEST) Message-Id: <62D492AB-ABD5-4A66-BE41-6191D5813AA5@lasmea.univ-bpclermont.fr> From: =?ISO-8859-1?Q?Jocelyn_S=E9rot?= To: OCaML Mailing List In-Reply-To: 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:23:56 +0200 References: <10F5DBD5-5387-408C-967B-50B37367A6E1@lasmea.univ-bpclermont.fr> <4E806C6F.5050407@gmail.com> <4FAB50A9-43BE-402D-8420-524573F10668@lasmea.univ-bpclermont.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 p8R8O0Dm003415 X-Validation-by: jocelyn.serot@ubpmes.univ-bpclermont.fr Subject: Re: [Caml-list] Dependent types ? Le 26 sept. 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. Yes. Good point. Thanks for the idea. IIUC, my add function would be declared as : val add : 'a sized_int * 'a sized_int -> 'a sized_int then, with val x : size16 sized_int val y : size16 sized_int the type infered for z in let z = add (x,y) will be z : size16 sized_int Am i right ? > > 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. Thanks for the pointer. I'll have a look at this. But i'm afraid that this would require a too profound change in the implementation of the type system.. Jocelyn > > > 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 >>> >> >>