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 p8TAvZhv027969 for ; Thu, 29 Sep 2011 12:57:35 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AtUBAPlNhE7D3XqWi2dsb2JhbABBgk2lPxQBAQEKCwsbJYFTAQEEASdXCx0GIAENHyoECgYuh18CuAOGMmEEjAiHToUjjBk X-IronPort-AV: E=Sophos;i="4.68,460,1312149600"; d="scan'208,217";a="122122601" Received: from ubpmes.univ-bpclermont.fr ([195.221.122.150]) by mail1-smtp-roc.national.inria.fr with ESMTP; 29 Sep 2011 12:57:35 +0200 Received: from localhost (localhost.localdomain [127.0.0.1]) by ubpmes.univ-bpclermont.fr (Postfix) with ESMTP id CB6D0545BBE for ; Thu, 29 Sep 2011 12:57:34 +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 ab7x+--s49fz for ; Thu, 29 Sep 2011 12:57:32 +0200 (CEST) Received: from [172.27.1.69] (unknown [193.54.50.250]) by ubpmes.univ-bpclermont.fr (Postfix) with ESMTP id 5CAC6545A56 for ; Thu, 29 Sep 2011 12:57:32 +0200 (CEST) Message-Id: <785DC134-4170-4B3A-A20D-EEAE48D6E26B@lasmea.univ-bpclermont.fr> From: =?ISO-8859-1?Q?Jocelyn_S=E9rot?= To: OCaML Mailing List Content-Type: multipart/alternative; boundary=Apple-Mail-4--315764416 Mime-Version: 1.0 (Apple Message framework v935.3) Date: Thu, 29 Sep 2011 12:57:31 +0200 References: <3522CB9B-B4B4-43EA-BFCA-C0553A5D4636@lasmea.univ-bpclermont.fr> X-Mailer: Apple Mail (2.935.3) X-Validation-by: jocelyn.serot@ubpmes.univ-bpclermont.fr Subject: Fwd: [Caml-list] Dependent types ? --Apple-Mail-4--315764416 Content-Type: text/plain; charset=ISO-8859-1; format=flowed; delsp=yes Content-Transfer-Encoding: quoted-printable Thanks to all for the propositions ! I think I need to give a more concrete example to explain my pb and=20=20 wishes. Sorry, if this get a bit longish. So, here's a small example in CAPH, involving a very single actor,=20=20 performing addition on streams of signed, 8-bit integers : ---------- sizedint.cph ----------- actor foo () in (a:signed<8>, b:signed<8>) out (c:signed<8>) rules (a, b) -> c | (x, y) -> x+y ; stream i1:signed<8> from "sample1.txt"; stream i2:signed<8> from "sample2.txt"; stream o:signed<8> to "result.txt"; net o =3D foo (i1,i2); ---------- ------------ ----------- The VHDL code inferred for this example. In particular, the code=20=20 describing the behavior of the foo actor will contain lines (lots of=20=20 lines omitted here) : ---------- foo_act.vhd ----------- entity foo_act is port ( ... a: in std_logic_vector(7 downto 0); b: in std_logic_vector(7 downto 0); c: out std_logic_vector(7 downto 0); ... ); end foo_act; architecture FSM of foo_act is ... variable x_v : std_logic_vector(7 downto 0); variable y_v : std_logic_vector(7 downto 0); ... c <=3D x_v + y_v; ... end FSM; ---------- ------------ ----------- If i replace 8 by 16 in the .cph source code, the generated code will=20=20 be similar, except that the std_logic_vectors will (correctly) have=20=20 range "15 downto 0". The genericity of the "+" operator does the rest. So far, so good. But now suppose that the foo actor, instead of using directly the "+"=20=20 operator calls a user-defined "add" function (which itself uses the=20=20 "+" operator). Here's the way to write this in CAPH : ---------- sizedint.cph ----------- function add (x,y) =3D x+y : signed<8> * signed<8> -> signed<8>; actor foo () in (a:signed<8>, b:signed<8>) out (c:signed<8>) rules (a, b) -> c | (x, y) -> add(x,y) ; stream i1:signed<8> from "sample1.txt"; stream i2:signed<8> from "sample2.txt"; stream o:signed<8> to "result.txt"; net o =3D foo (i1,i2); ---------- ------------ ----------- Again, this compiles and runs ok, with the an extra VHDL file=20=20 generated, called sizedint_globals.vhd : ---------- sizedint_globals.vhd ----------- package sizedint_globals is function add(x:std_logic_vector(7 downto 0); y:std_logic_vector(7=20=20 downto 0)) return std_logic_vector; end sizedint_globals; package body sizedint_globals is function add(x:std_logic_vector(7 downto 0); y:std_logic_vector(7=20=20 downto 0)) return std_logic_vector is begin return x + y; end add; end sizedint_globals; ---------- ------------ ----------- But now, suppose i now want to write the same program for 16 bit=20=20 integers (as Oliver rightly points it out, one major advantage of hw=20=20 programming is the ability to adjust datapath to applications to avoid=20= =20 waste of ressources). For this, i will have to rewrite ---------- sizedint.cph ----------- function add (x,y) =3D x+y : signed<16> * signed<16> -> signed<16>; actor foo () in (a:signed<16>, b:signed<16>) out (c:signed<16>) rules (a, b) -> c | (x, y) -> add(x,y) ; stream i1:signed<16> from "sample1.txt"; stream i2:signed<16> from "sample2.txt"; stream o:signed<16> to "result.txt"; net o =3D foo (i1,i2); ---------- ------------ ----------- Of course, changing the type signature for foo and the I/Os is normal=20=20 (after all, it's what i want). But I would to like to avoid writing another add function (because i=20=20 know that, at the VHDL level, my function is generic in size). So i would like to be able to write sth like : ---------- sizedint.cph ----------- function add (x,y) =3D x+y : signed * signed -> signed; ... ---------- ------------ ----------- and let the compiler infer, from the context in which add is called=20=20 the value of s (and generated the right signature and impl in=20=20 signedint_globals.vhd). Jocelyn Le 27 sept. 11 =E0 16:13, oliver a =E9crit : > Hello, > > > On Tue, Sep 27, 2011 at 10:23:56AM +0200, Jocelyn S=E9rot wrote: >> >> Le 26 sept. 11 =E0 18:44, Gabriel Scherer a =E9crit : >> >>>> Phantom types could be a solution but we must declare a new type=20=20 >>>> for >>>> each possible size, which is cumbersome / annoying. >>> >>> If you define the type system yourself, you can easily add a=20=20 >>> family of >>> type constants `size` (with `n` an integer literal) to the=20=20 >>> default >>> environment of the type checker. Then you can define a parametrized >>> type `type 's sized_int` (or float, etc.) and instantiate it with=20=20 >>> 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 =3D add (x,y) >> >> will be >> >> z : size16 sized_int >> >> Am i right ? > [...] > > Not sure. > > Depends on what you want ;-) > > What would the type system > yield fopr a type for > > > > val x : size16 sized_int > val y : size16 sized_int > > let z =3D and_msb (x,y) # AND the MSBs of both input values > > z might be 16 Bits, if this is your "natural" int size - but: what=20=20 > is natural on > FPGA's, when you can change your HW at will? > And: if it's "batural", why to declare it? > > But ANDing two Bits will result in a 1 Bit result. > > Why should z be 16 Bits then? > That would be wasting ressources. > > IMHO it does not make sense to derive the type of z from the type of > x and y. It must be derived from the operation or function that is=20=20 > used. > > > If you use 'a sized_int then this would offer you > the possibility also of taking 2 x 16 Bits and get 1 Bit (as in the=20=20 > and_msb()-example) > but of course also to do your > > z =3D add (x,y) with z of 16 Bits, which you looked for. > > But is thats a type that can be derived from x and y? > > Or is it rather the OPERATION ("add" here), or better: the operation > together with the input values, that fives you the resulting type? > > What if you do: > > val x : size16 sized_int > val y : size8 sized_int > > z =3D add(x, y) > > What type does z no have? > > 8 Bits? 16 Bits? > Somewhere in between? > > > AFAIK one of the biggest (or better: THE) advantage of FPGAs/VHDL is: > you can create your "HW" (HW connections) by SW. > > So you are not fixed in width, and you can save some bits here and=20=20 > there, > and use them later somewhere else... > > > And, I doubt, somehow, that what you are talking about is a "type=20=20 > issue". > At least nothing that can be derived from the structure of the inputs > without knowing the operation. > > AFAIK you are not constrained to a fixed ALU and databus width, > at least not in a sense as we know it from fixed HW that we normally=20= =20 > use > when buying a computer at the store. > (There may be limits of course, depending on the FPGA device in use.) > > > So, how do you address these issues? > > I would say either you also need to define the type of z, > or you need to derive the type from the source of which > your operations/functions are derived. > > So: you need more information than what you presented in your=20=20 > questions, > to decide for the resulting type. > > Ciao, > Oliver --Apple-Mail-4--315764416 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable
Thanks to all for the propositions !

I think I need to give a more concrete example to= explain my pb and wishes.
Sorry, if this get a bit longish.

So, here's a small example in CAPH, involving a very s= ingle actor, performing addition on streams of signed, 8-bit integers :

-------= --- sizedint.cph -----------

actor foo ()
  in (a:signed<8>, b:s= igned<8>)
  out (c:signed<8>)
rules
  (a, b) -> c
| (x, y)= -> x+y
;

stream i1:signed<8> from "sample1.txt";
stream i2:signed<8> from = "sample2.txt";
stream o:signed<8> to "result.txt";

net o =3D foo= (i1,i2);

---------- ------------ -----------

The VHDL= code inferred for this example. In particular, the code describing the beh= avior of the foo actor will contain lines (lots of lines omitted here) :

= ---------- foo_act.vhd  -----------

entity foo_act is
   port (=
  = ;  ...
    a: in std_logic_vector(7 downto 0);
<= span class=3D"Apple-style-span" style=3D"font-size: 12px;">  &nbs= p; b: in std_logic_vector(7 downto 0);
    c: out std_l= ogic_vector(7 downto 0);
    ...    );<= /div>
end foo_act;=

=
= architecture FSM of foo_act is
   ...
    variable x_v : std= _logic_vector(7 downto 0);
    variable y_v : std_logic_vector(7 = downto 0);
    ...
    c <=3D x_v + y_v;=
  = ; ...
end FSM;

---------- ------------ -= ----------

If i replace 8 by 16 in the .cph sour= ce code, the generated code will be similar, except that the std_logic_vect= ors will (correctly) have range "15 downto 0".
The genericity of = the "+" operator does the rest.

So far, so good.

But now suppose that the foo actor, instead of usin= g directly the "+" operator calls a user-defined "add" function (which itse= lf uses the "+" operator).

Here's the way to write= this in CAPH : 

---------- sizedint.cph -----------

function add= (x,y) =3D x+y : signed<8> * signed<8> -> signed<8>;

actor = foo ()
  out (c:signe= d<8>)
rules
  (a, b) -> c
| (x, y) -> add(x,y)
=
;

stream i1:signed<8> from "sample1.txt";
stream i2:signed<8> from = "sample2.txt";
stream o:signed<8> to "result.txt";

net o =3D foo (i1,i2);

---------- ------------ -----------

Again, this compiles and runs ok, wit= h the an extra VHDL file generated, called sizedint_globals.vhd :

---------- sizedint_globals.vhd -----------
=
package sizedint_glob= als is
end sizedint_globals;

package body sizedint_= globals is
  function add(x:std_logic_vector(7 downto 0); y:std_logic_= vector(7 downto 0)) return std_logic_vector is
  begin
    r= eturn x + y;
  end add;
end sizedint_globals;

=
---------- -= ----------- -----------

But no= w, suppose i now want to write the same program for 16 bit integers (as Oli= ver rightly points it out, one major advantage of hw programming is the abi= lity to adjust datapath to applications to avoid waste of ressources).
For this, i will have to rewrite 

=
---------- sizedint.cph= -----------

function add (x,y) =3D x+y : signed<16> * signed<= ;16> -> signed<16>;

actor foo ()
  in (a:signed<16>, b= :signed<16>)
  out (c:signed<16>)
rules
=
  (a, b) ->= ; c
= | (x, y) -> add(x,y)
;
=
stream i1:signed<16>= ; from "sample1.txt";
stream i2:signed<16> from "sample2.txt";
= stream o:signe= d<16> to "result.txt";

net o =3D foo (i1,i2);
----------= ------------ -----------
 <= /div>
Of course, changing the type signature for foo and the I/Os is no= rmal (after all, it's what i want).
But I would to like to avoid = writing another add function (because i know that, at the VHDL level, my fu= nction is generic in size).
So i would like to be able to write s= th like :

---------- sizedint.cph -----------

=
function add (x,y)= =3D x+y : signed<s> * signed<s> -> signed<s>;<= /font>

...<= /div>

---------- ------------ ---------= --

a= nd let the compiler infer, from the cont= ext in which add is called the value of s (an= d generated the right signature and impl in signedint_globals.vhd).

Jocelyn

 Le 27 sept. 11 =E0= 16:13, oliver a =E9crit :

Hello,


On Tue,= Sep 27, 2011 at 10:23:56AM +0200, Jocelyn S=E9rot wrote:

Le 26 sept. 11 =E0 1= 8:44, Gabriel Scherer a =E9crit :

Phantom types could be a solution but we must declare = a new type for
each possible= size, which is cumbersome / annoying.

=
If you def= ine the type system yourself, you can easily add a family of
type con= stants `size<n>` (with `n` an integer literal) to the default
e= nvironment of the type checker. Then you can define a parametrized
ty= pe `type 's sized_int` (or float, etc.) and instantiate it with any
o= f the size<n>.

Yes. Good point. Thanks for the= idea.
IIUC, my add function woul= d be declared as :

val add : 'a sized_int * 'a sized_int -> 'a= sized_int

then, with
<= br>
val x : size16 sized_int
val y : size16 sized_int
=

the ty= pe infered for z in

let z =3D add (x,y)

will be

z : size16 sized_int

Am i right ?
[...]
Not sure.

Depends on what you want ;-)

What would the type s= ystem
yield fopr a type for



val x : size16 sized_int
v= al y : size16 sized_int

let z =3D and_msb (x,y)  # AND the MSBs= of both input values

z might be 16 Bits, if this is your "natural" = int size - but: what is natural on
FPGA's, when you can change your HW a= t will?
And: if it's "batural", why to declare it?

But ANDing two= Bits will result in a 1 Bit result.

Why should z be 16 Bits then?That would be wasting ressources.

IMHO it does not make sense to d= erive the type of z from the type of
x and y. It must be derived from th= e operation or function that is used.


If you use  'a sized_= int   then  this would offer you
the possibility also of = taking 2 x 16 Bits and get 1 Bit (as in the and_msb()-example)
but of co= urse also to do your

z =3D add (x,y) with z of 16 Bits, which you lo= oked for.

But is thats a type that can be derived from x and y?
<= br>Or is it rather the OPERATION ("add" here), or better: the operation
= together with the input values, that fives you the resulting type?

W= hat if you do:

val x : size16 sized_int
val y : size8  sized= _int

z =3D add(x, y)

What type does z no have?

8 Bits?= 16 Bits?
Somewhere in between?


AFAIK one of the biggest (or = better: THE) advantage of FPGAs/VHDL is:
you can create your "HW" (HW co= nnections) by SW.

So you are not fixed in width, and you can save so= me bits here and there,
and use them later somewhere else...


= And, I doubt, somehow, that what you are talking about is a "type issue".At least nothing that can be derived from the structure of the inputs
= without knowing the operation.

AFAIK you are not constrained to a fi= xed ALU and databus width,
at least not in a sense as we know it from fi= xed HW that we normally use
when buying a computer at the store.
(The= re may be limits of course, depending on the FPGA device in use.)

So, how do you address these issues?

I would say either you also n= eed to define the type of z,
or you need to derive the type from the sou= rce of which
your operations/functions are derived.

So: you need = more information than what you presented in your questions,
to decide fo= r the resulting type.

Ciao,
  Oliver


= --Apple-Mail-4--315764416--