[Caml-list] Dependent types ?

["Damien Guichard" <alphablock@orange.fr>]

[-- Attachment #1.1: Type: text/plain, Size: 2869 bytes --]

That's pretty cool, everyone and his mother has a solution to the proposed problem.
I think, for the sake of exhaustivity, i can share my own weird hack.
It can express all power of 2 sizes (for example add, mul and div).
It uses a nested data type.


  type 'a size =
   | Word of 'a
   | DWord of ('a * 'a) size

   type n16 = int size
   type n32 = (n16 * n16) size
   type n64 = (n32 * n32) size

   add : 'a size -> 'a size -> 'a size 
   mul : 'a size -> 'a size -> ('a * 'a) size 
   div : ('a * 'a) size -> 'a size -> ('a size * 'a size)


- damien


Le 26/09/2011 à 13:42, "Jocelyn Sérot"  à écrit :
>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
>).
>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
>
>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 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 (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 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 trivial" ! ;-) - will be 
>appreciated.
>
>Best wishes
>
>Jocelyn
>
>(1) i.e. i dont bother supporting declarations like : val mul : 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
>


--
Mail created using EssentialPIM Free - www.essentialpim.com

[-- Attachment #1.2: Type: text/html, Size: 4090 bytes --]