Re: [Caml-list] Dependent types ?

[oliver <oliver@first.in-berlin.de>]

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