From mboxrd@z Thu Jan 1 00:00:00 1970 X-Sympa-To: caml-list@inria.fr 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 p8QL9MBE008584 for ; Mon, 26 Sep 2011 23:09:22 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ArIBAPLogE5KfVK2imdsb2JhbABCFoRMlBOOcQgUAQEBCgkNBxIGIoFTAQEBAQIBEgIPBBkBCBMSCgIDDAYFEAgJBA8DCwICAgcDAgECAQ8CEQEFAQIIEhMGAgEBDgkHh1YCBJ1VCosIRIJchSM7iG4CAwaDEoJigREEjjqLZINLgnI9g28 X-IronPort-AV: E=Sophos;i="4.68,446,1312149600"; d="asc'?vcf'?scan'208";a="110627443" Received: from mail-wy0-f182.google.com ([74.125.82.182]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 26 Sep 2011 23:09:16 +0200 Received: by wyj26 with SMTP id 26so5760884wyj.27 for ; Mon, 26 Sep 2011 14:09:16 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=message-id:date:from:user-agent:mime-version:to:subject:references :in-reply-to:x-enigmail-version:content-type; bh=VbHGYd2Qfw031F8zDo37e7pJbW5lTzCO8TbjaY7XOOs=; b=kZXB5ZSkht7UN3VnKlYhICoCb+enHYWo6vngw4x0YuFCClz3SaOKiukhjJ8G7vNtkW krPXvYjs47/sx3jiSoBBbe+H6zSn0PcN4mlLxxWk0scQiG2nljsTVk+ubn9Uj3MHaDZw hAI1vSjZf6fc07WxYe9sn+xiOODxiSK+X+v90= Received: by 10.227.195.145 with SMTP id ec17mr5177349wbb.0.1317071356541; Mon, 26 Sep 2011 14:09:16 -0700 (PDT) Received: from Tocksi.local (bin73-1-78-240-16-62.fbx.proxad.net. [78.240.16.62]) by mx.google.com with ESMTPS id y10sm32803120wbm.14.2011.09.26.14.09.14 (version=TLSv1/SSLv3 cipher=OTHER); Mon, 26 Sep 2011 14:09:15 -0700 (PDT) Message-ID: <4E80E9F4.4050507@univ-savoie.fr> Date: Mon, 26 Sep 2011 23:09:08 +0200 From: Christophe Raffalli User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:6.0.2) Gecko/20110902 Thunderbird/6.0.2 MIME-Version: 1.0 To: caml-list@inria.fr References: <10F5DBD5-5387-408C-967B-50B37367A6E1@lasmea.univ-bpclermont.fr> <4E806C6F.5050407@gmail.com> <4FAB50A9-43BE-402D-8420-524573F10668@lasmea.univ-bpclermont.fr> In-Reply-To: X-Enigmail-Version: 1.3.1 Content-Type: multipart/signed; micalg=pgp-sha1; protocol="application/pgp-signature"; boundary="------------enigF4C4D23489C69E2281E5145B" X-Validation-by: craff73@gmail.com Subject: Re: [Caml-list] Dependent types ? This is an OpenPGP/MIME signed message (RFC 2440 and 3156) --------------enigF4C4D23489C69E2281E5145B Content-Type: multipart/mixed; boundary="------------080106030207040002020309" This is a multi-part message in MIME format. --------------080106030207040002020309 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Hello, Le 26/09/11 18:44, Gabriel Scherer a =C3=A9crit : >> 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 `=E2=98=85`, 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 `=E2=98=85` for types of one machine word, `=E2=98=852` for two ma= chine > 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 =E2=80=93 unless you introduce kind polymorp= hism, > 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=C3=A9rot > 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 w= hat >> 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 c= ould >> hack the following definitions (from types. ml) >> type typ =3D >> | TyVar of typ_var >> | TyTerm of string * typ list >> and typ_var =3D >> { mutable level: int; >> mutable value: tyvar_value } >> and tyvar_value =3D >> | Unknown >> | Known of typ >> by adding a notion of "size variable" (sorry if this sounds imprecise, t= his >> is still a but hazy in my mind..) >> type typ =3D >> | TyVar of typ_var >> | TyTerm of string * typ list * typ_size >> and typ_sz =3D >> { mutable value: tysz_value } >> and tyvar_value =3D >> | 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 =C3=A0 14:45, Yaron Minsky a =C3=A9crit : >> >> 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 typ= es >> 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 >>> =3D >>> struct >>> type 'a integer =3D int >>> >>> let int16 x =3D x >>> let int32 x =3D x >>> >>> let add x y =3D x + y >>> end >>> >>> then >>> >>> open SizedInt >>> >>> let bar =3D >>> let x =3D int16 42 in >>> foo x >>> >>> must have type i16 integer -> i16 integer >>> >>> Regards, >>> >>> Denis Berthod >>> >>> >>> Le 26/09/2011 13:42, Jocelyn S=C3=A9rot a =C3=A9crit : >>>> 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 =3D 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 >>> >> > --=20 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=20 can check this signature. The public key is stored on www.keyserver.net --------------------------------------------- --------------080106030207040002020309 Content-Type: text/x-vcard; charset=utf-8; name="Christophe_Raffalli.vcf" Content-Transfer-Encoding: base64 Content-Disposition: attachment; filename="Christophe_Raffalli.vcf" YmVnaW46dmNhcmQNCmZuOkNocmlzdG9waGUgUmFmZmFsbGkNCm46UmFmZmFs bGk7Q2hyaXN0b3BoZQ0Kb3JnOkxBTUEgKFVNUiA1MTI3KQ0KZW1haWw7aW50 ZXJuZXQ6Y2hyaXN0b3BoZS5yYWZmYWxsaUB1bml2LXNhdm9pZS5mcg0KdGl0 bGU7cXVvdGVkLXByaW50YWJsZTpNYT1DMz1BRXRyZSBkZSBjb25mPUMzPUE5 cmVuY2VzDQp0ZWw7d29yazorMzMgNCA3OSA3NSA4MSAwMw0Kbm90ZTpodHRw Oi8vd3d3LmxhbWEudW5pdi1zYXZvaWUuZnIvfnJhZmZhbGxpDQp4LW1vemls bGEtaHRtbDpUUlVFDQp2ZXJzaW9uOjIuMQ0KZW5kOnZjYXJkDQoNCg== --------------080106030207040002020309-- --------------enigF4C4D23489C69E2281E5145B Content-Type: application/pgp-signature; name="signature.asc" Content-Description: OpenPGP digital signature Content-Disposition: attachment; filename="signature.asc" -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.7 (Darwin) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/ iD8DBQFOgOn5i9jr/RgYAS4RAg1EAJ40x7LTawGgqJLDfg8TUJ5NLOgTVwCgq9/a QNwqXNTC6O3I/decit4XuY4= =59fN -----END PGP SIGNATURE----- --------------enigF4C4D23489C69E2281E5145B--