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 p8R8Ra0C003720 for ; Tue, 27 Sep 2011 10:27:36 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AjoCANiHgU7D3XqWmWdsb2JhbABBh02RMjWHGgGHLRQBAQEBAQgLCwcUJoFTAQEEASdHEAsLGA0hHwIkEgYTEodmAgS5FYMYgxNgBIJUiTOHS4UihHaFc4Er X-IronPort-AV: E=Sophos;i="4.68,448,1312149600"; d="scan'208,217";a="121644809" Received: from ubpmes.univ-bpclermont.fr ([195.221.122.150]) by mail1-smtp-roc.national.inria.fr with ESMTP; 27 Sep 2011 10:27:30 +0200 Received: from localhost (localhost.localdomain [127.0.0.1]) by ubpmes.univ-bpclermont.fr (Postfix) with ESMTP id DCD352C06AE for ; Tue, 27 Sep 2011 10:27:30 +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 dT0FlW+uGWeF for ; Tue, 27 Sep 2011 10:27:29 +0200 (CEST) Received: from [172.27.1.69] (unknown [193.54.50.250]) by ubpmes.univ-bpclermont.fr (Postfix) with ESMTP id 4D0782C314A for ; Tue, 27 Sep 2011 10:27:29 +0200 (CEST) Message-Id: From: =?ISO-8859-1?Q?Jocelyn_S=E9rot?= To: OCaML Mailing List In-Reply-To: Content-Type: multipart/alternative; boundary=Apple-Mail-7--497566791 Mime-Version: 1.0 (Apple Message framework v935.3) Date: Tue, 27 Sep 2011 10:27:29 +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-7--497566791 Content-Type: text/plain; charset=ISO-8859-1; format=flowed; delsp=yes Content-Transfer-Encoding: quoted-printable 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. > In the current situation, this will be handled at the VHDL level. Making it explicit at CAPH (the source level DSL) would be great but=20=20 i'm afraid it is too complex to implement for the moment. > 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-7--497566791 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable
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 th= at requires 17 bits.


In the current situatio= n, this will be handled at the VHDL level. 
Making it explic= it at CAPH (the source level DSL) would&= nbsp;be great but i'm afraid it is too&n= bsp;complex to implement for the moment.

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" <denis.berthod@gmail.com> wrote:
> Hello,
>
> I think that achieving something ve= ry near from what you whant is
> relatively easy using phantom type= s.
> That avoid the boxing/unboxing in records.
>
> type= i16
> type i32
>
> module SizedInt:
> sig> type 'a integer
> val int16: int -> i16 inte= ger
> val int32: int -> i32 integer
> val ad= d: 'a integer -> 'a integer -> 'a integer
> end
> = =3D
> struct
> type 'a integer =3D int
> <= br>> let int16 x =3D x
> let int32 x =3D x
&g= t;
> 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,
>
> D= enis 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.f= r/Personnel/Jocelyn.Serot/caph.html).
>> The idea is to exten= d 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 wit= h variable bit width and I'd like to reflect this
>> in the sourc= e language.
>>
>> For instance, I'd like to be able to de= clare :
>>
>> val foo : int * int -> int
>><= br>>> (where the type int is not annotated, i.e. "generic")
>&g= t;
>> 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)
>>
>> the= n the compiler will infer type int<16> for z
>>
>>= In fact, the exact type signature for foo would be :
>>
>&g= t; 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 map : 'a list -> ('a ->= 'b) -> 'b list).
>>
>> In a sense, it has to do with t= he theory of sized types (Hughes and
>> Paretto, .. ) and depende= nt types (DML for ex), but my goal is far
>> less ambitious.
= >> In particular, i dont want to do _computations_ (1) on the size (a= nd,
>> a fortiori, don't want to prove anything on the programs).=
>> So sized types / dependent types seems a big machinery for a <= br> >> relatively small goal.
>> My intuition is that this i= s 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 tr= ivial" ! ;-) - will be
>> appreciated.
>>
>> Be= st wishes
>>
>> Jocelyn
>>
>> (1) i.e.= i dont bother supporting declarations like : val mul : int<n>
&g= t;> * int<n> -> int <2*n> ...
>>
>>
= >>
>
>
> --
> Caml-list mailing list. Su= bscription management and archives:
> https://sympa-roc.inria.fr/wws/info/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug re= ports: http://caml.inria.fr/= bin/caml-bugs
>

= --Apple-Mail-7--497566791--