Re: [Caml-list] Dependent types ?

[Denis Berthod <denis.berthod@gmail.com>]

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

Le 28/09/2011 00:12, Damien Guichard a écrit :
>
> 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)

div (2. ** 32.) 1. might be a problem here.

Denis.

> - 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 
> <http://www.essentialpim.com> 


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