Fwd: [Caml-list] Dependent types ?

Fwd: [Caml-list] Dependent types ?

[Jocelyn Sérot]

[-- Attachment #1: Type: text/plain, Size: 7470 bytes --]

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 single actor,  
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 = foo (i1,i2);

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

The VHDL code inferred for this example. In particular, the code  
describing the behavior 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);
     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 <= x_v + y_v;
    ...
end FSM;

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

If i replace 8 by 16 in the .cph source code, the generated code will  
be similar, except that the std_logic_vectors 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 using directly the "+"  
operator calls a user-defined "add" function (which itself uses the  
"+" operator).

Here's the way to write this in CAPH :

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

function add (x,y) = 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 = foo (i1,i2);

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

Again, this compiles and runs ok, with the an extra VHDL file  
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  
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  
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  
integers (as Oliver rightly points it out, one major advantage of hw  
programming is the ability to adjust datapath to applications to avoid  
waste of ressources).
For this, i will have to rewrite

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

function add (x,y) = 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 = foo (i1,i2);

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

Of course, changing the type signature for foo and the I/Os is normal  
(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 function is generic in size).
So i would like to be able to write sth like :

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

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

...

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

and let the compiler infer, from the context in which add is called  
the value of s (and generated the right signature and impl in  
signedint_globals.vhd).

Jocelyn

  Le 27 sept. 11 à 16:13, oliver a écrit :

> Hello,
>
>
> On Tue, Sep 27, 2011 at 10:23:56AM +0200, Jocelyn Sérot wrote:
>>
>> Le 26 sept. 11 à 18:44, Gabriel Scherer a écrit :
>>
>>>> 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<n>` (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<n>.
>>
>> 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 = 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 = 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 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  
> 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 course also to do your
>
> z = 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 = 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  
> 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 fixed ALU and databus width,
> at least not in a sense as we know it from fixed HW that we normally  
> 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  
> questions,
> to decide for the resulting type.
>
> Ciao,
>   Oliver



[-- Attachment #2: Type: text/html, Size: 22938 bytes --]