Re: [Caml-list] Dependent types ?

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

On Mon, Sep 26, 2011 at 01:42:51PM +0200, Jocelyn Sérot wrote:
> 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
[...]

Very interesting.

I also once thought about something like high level language support for
VHDL... when I one day would have time to learn VHDL.

Maybe I will be one of your CAPH users one day ;)


> ).
> The idea is to extend 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 with variable bit width and I'd like to reflect
> 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 = foo (x,y)
> 
> then the compiler will infer type int<16> for z
[...]

Hmhhh, not sure that z has size 16 Bits,
it might be more or less, depending on the operation that foo
will do.

And also I think, this type checking stuff is done somewhere
on your AST; maybe relying on OCaml directly here, might be problematic.


Ciao,
   Oliver