Re: [Caml-list] Dependent types ?

[Thomas Braibant <thomas.braibant@gmail.com>]

Hi,

There was a somewhat related discussion some time ago:

http://caml.inria.fr/pub/ml-archives/caml-list/2010/05/b2f6dda2453f395a23e0fbbc988a2e0a.en.html

The idea was to define something like  :
type n16
type n32
type n64
type 'a sint = { value : int};; (*  the record here is important *)
let sint_plus (x : 'a sint) ( y : 'a sint) : 'a sint = {value =
x.value + y.value};;

With this solution you can not make computation the size, but it may
be sufficient for your needs.
Hope this helps.
Thomas Braibant



On Mon, Sep 26, 2011 at 1:42 PM, Jocelyn Sérot
<Jocelyn.SEROT@ubpmes.univ-bpclermont.fr> 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).
> 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<s> * int <s> -> int<s>
>
> 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<n> *
> int<n> -> 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
>
>