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 p8QFtIp5000459 for ; Mon, 26 Sep 2011 17:55:18 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AnACAB+fgE7D3XqWmWdsb2JhbABBgk2Ef5FNNYcaAYcoFAEBAQEBCAsLBxQmgVMBAQQBJ0cQCwsYDSEfAiQSBhMSCYddAgS6R4MYgxNgBIJUiTOHS4UihHWFc4Er X-IronPort-AV: E=Sophos;i="4.68,445,1312149600"; d="scan'208,217";a="110586655" Received: from ubpmes.univ-bpclermont.fr ([195.221.122.150]) by mail4-smtp-sop.national.inria.fr with ESMTP; 26 Sep 2011 17:55:08 +0200 Received: from localhost (localhost.localdomain [127.0.0.1]) by ubpmes.univ-bpclermont.fr (Postfix) with ESMTP id D92147C5AAD for ; Mon, 26 Sep 2011 17:55:07 +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 UPen9gxwqJ74 for ; Mon, 26 Sep 2011 17:55:06 +0200 (CEST) Received: from [172.27.1.69] (unknown [193.54.50.250]) by ubpmes.univ-bpclermont.fr (Postfix) with ESMTP id 39D6E7C5AAC for ; Mon, 26 Sep 2011 17:55:06 +0200 (CEST) Message-Id: <4FAB50A9-43BE-402D-8420-524573F10668@lasmea.univ-bpclermont.fr> From: =?ISO-8859-1?Q?Jocelyn_S=E9rot?= To: OCaML Mailing List In-Reply-To: Content-Type: multipart/alternative; boundary=Apple-Mail-5--557110320 Mime-Version: 1.0 (Apple Message framework v935.3) Date: Mon, 26 Sep 2011 17:55:05 +0200 References: <10F5DBD5-5387-408C-967B-50B37367A6E1@lasmea.univ-bpclermont.fr> <4E806C6F.5050407@gmail.com> X-Mailer: Apple Mail (2.935.3) X-Validation-by: jocelyn.serot@ubpmes.univ-bpclermont.fr Subject: Re: [Caml-list] Dependent types ? --Apple-Mail-5--557110320 Content-Type: text/plain; charset=ISO-8859-1; format=flowed; delsp=yes Content-Transfer-Encoding: quoted-printable Thanks to all for your answers. Phantom types could be a solution but we must declare a new type for=20=20 each possible size, which is cumbersome / annoying. Moreover, since i'm writing a DSL, the fact that they do not require a=20= =20 modification to the existing type system is not really an advantage. My language has its own type system (largely inspired from OCaml's) so=20= =20 what I was looking for was more a way to modify the type=20=20 representation to support the requested behavior. To those familiar with Caml compiler source code, i was wondering if i=20= =20 could 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,=20= =20 this 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=20=20 extension yet. Jocelyn Le 26 sept. 11 =E0 14:45, Yaron Minsky a =E9crit : > As written, the behavior of the types might not be what you expect,=20=20 > since addition of two 16 bit ints may result in an int that requires=20= =20 > 17 bits. > > When using phantom types, you need to be especially careful that the=20= =20 > types mean what you think they mean. > > On Sep 26, 2011 8:13 AM, "Denis Berthod" =20=20 > 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=E9rot a =E9crit : > >> 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= =20 > ). > >> The idea is to extend the type system to accept "size"=20=20 > 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=20= =20 > 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=20= =20 > 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=20=20 > (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=20=20 > which > >> the variables ranged over are not types but integers. > >> Before testing this intuition by trying to implement it, I'd like=20= =20 > 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 :=20=20 > 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 > > --Apple-Mail-5--557110320 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Thanks to all for your answers.
Phantom types could be a solution but we must declare a new typ= e for each possible size, which is cumbersome / annoying.

Moreover, since i'm writing a DSL, the fact that they do not requir= e 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 famil= iar with Caml compiler source code, i was wondering if i could hack the fol= lowing definitions (from types. ml)

type typ =3D
   | TyVar of typ_var
 &n= bsp; | TyTerm of string * typ list 

and typ_var =3D
  { muta= ble 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 impreci= se, this is still a but hazy in my mind..)

type typ =3D
   | TyVar = of typ_var
   | TyTerm of string * typ list * typ_size 

and ty= p_sz =3D
  { mutable value: tysz_value }

<= div>and tyvar_value =3D
 &= nbsp;| Unknown
  | Known of int
<= br>
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 =E0 14:45, Yaron Minsky a =E9crit :

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 Bertho= d" <denis.berthod@gmail.com> wrote:
> Hello,
>
> I think = that achieving something very near from what you whant is
> relativ= ely easy using phantom types.
> That avoid the boxing/unboxing in rec= ords.
>
> type i16
> type i32
>
> module Si= zedInt:
> sig
> type 'a integer
> val= int16: int -> i16 integer
> val int32: int -> i32 int= eger
> val add: 'a integer -> 'a integer -> 'a integer<= br>> 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
&= gt;
> must have type i16 integer -> i16 integer
>
> = Regards,
>
> Denis Berthod
>
>
> Le 26/09/= 2011 13:42, Jocelyn S=E9rot a =E9crit :
>> Hello,
>>
= >> I've recently come across a problem while writing a domain specifi= c
>> language for hardware synthesis
>> (http://= wwwlasmea.univ-bpclermont.fr/Personnel/Jocelyn.Serot/caph.html).
&g= t;> The idea is to extend the type system to accept "size" annotations f= or
>> int types (it could equally apply to floats).
>> T= he target language (VHDL in this case) accept "generic" functions,
>= ;> operating on ints with variable bit width and I'd like to reflect thi= s
>> 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)<= br>>>
>> then the compiler will infer type int<16> for= z
>>
>> In fact, the exact type signature for foo would= be :
>>
>> val foo : int<s> * int <s> -> = int<s>
>>
>> where "s" would be a "size variable" (= playing a role similar to a type
>> variable in, for ex : val ma= p : '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
&= gt;> less ambitious.
>> In particular, i dont want to do _compu= tations_ (1) on the size (and,
>> a fortiori, don't want to prove= anything on the programs).
>> So sized types / dependent types se= ems a big machinery for a
>> relatively small goal.
>> = My intuition is that this is just a variant of polymorphism in which
&g= t;> the variables ranged over are not types but integers.
>> Be= fore 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
&g= t;>
>> (1) i.e. i dont bother supporting declarations like : va= l mul : int<n>
>> * int<n> -> int <2*n> ...<= br>>>
>>
>>
>
>
> --
> = Caml-list mailing list. Subscription management and archives:
> https://sympa-roc.inr= ia.fr/wws/info/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_be= ginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>

= --Apple-Mail-5--557110320--