From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p8QGiZ7B002404 for ; Mon, 26 Sep 2011 18:44:36 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ao4BAN6qgE7RVdy2mGdsb2JhbABChGKUN45wCBQBAQEBAQgJDQcUJoFTAQEBAQIBEgIPBBkBEwgSCwEDAQsGBQsNAgIJHQICIQEBEQEFAQoSBhMSCQeHVgaeIwqLCESCXIUNO4huAgMGgSaBbIJigREEk1KKF4JyPYNv X-IronPort-AV: E=Sophos;i="4.68,445,1312149600"; d="scan'208";a="110594898" Received: from mail-vx0-f182.google.com ([209.85.220.182]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 26 Sep 2011 18:44:35 +0200 Received: by vcbf13 with SMTP id f13so5606823vcb.27 for ; Mon, 26 Sep 2011 09:44:34 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type:content-transfer-encoding; bh=ZsXX7zGJGLxRkh2si2sgwDHQQcAnXkP1mDN8sVVOg1s=; b=ZNCi9R2BVuzkkDMZ32pHwwYSxzjSvi7JqV9HeZ8d2ZONCT0OSK3mU+yPWLzg/bL/lS Qse33ggjXVPzhV2QSG8LjBEABC2OY6VnN4TOxOTBentX8b2GOsCBz7c7TUURrw3J4Uml P4N3RJPxj26aN9GLicGI3Ov05tKrxPj5Ws0OM= Received: by 10.52.97.194 with SMTP id ec2mr5358952vdb.379.1317055473234; Mon, 26 Sep 2011 09:44:33 -0700 (PDT) MIME-Version: 1.0 Received: by 10.52.168.197 with HTTP; Mon, 26 Sep 2011 09:44:13 -0700 (PDT) In-Reply-To: <4FAB50A9-43BE-402D-8420-524573F10668@lasmea.univ-bpclermont.fr> References: <10F5DBD5-5387-408C-967B-50B37367A6E1@lasmea.univ-bpclermont.fr> <4E806C6F.5050407@gmail.com> <4FAB50A9-43BE-402D-8420-524573F10668@lasmea.univ-bpclermont.fr> From: Gabriel Scherer Date: Mon, 26 Sep 2011 18:44:13 +0200 Message-ID: To: =?ISO-8859-1?Q?Jocelyn_S=E9rot?= Cc: OCaML Mailing List Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id p8QGiZ7B002404 Subject: Re: [Caml-list] Dependent types ? > 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. 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 >> > >