Re: [Caml-list] Dependent types ?

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

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

Indeed.

So you can have something like that in the module implementation:

type 'a interger = int * int

let int16 x = 16, x
let int32 x = 32, x

let add (size, x) (_, y) = treat_overflow (size, x + y)

Regards,

Denis Berthod

Le 26/09/2011 14:45, Yaron Minsky a écrit :
>
> As written, the behavior of the types might not be what you expect, 
> since addition of two 16 bit ints may result in an int that requires 
> 17 bits.
>
> When using phantom types, you need to be especially careful that the 
> types mean what you think they mean.
>
> On Sep 26, 2011 8:13 AM, "Denis Berthod" <denis.berthod@gmail.com 
> <mailto:denis.berthod@gmail.com>> wrote:
> > Hello,
> >
> > I think that achieving something very near from what you whant is
> > relatively easy using phantom types.
> > That avoid the boxing/unboxing in records.
> >
> > type i16
> > type i32
> >
> > module SizedInt:
> > sig
> > type 'a integer
> > val int16: int -> i16 integer
> > val int32: int -> i32 integer
> > val add: 'a integer -> 'a integer -> 'a integer
> > end
> > =
> > struct
> > type 'a integer = int
> >
> > let int16 x = x
> > let int32 x = x
> >
> > let add x y = x + y
> > end
> >
> > then
> >
> > open SizedInt
> >
> > let bar =
> > let x = int16 42 in
> > foo x
> >
> > must have type i16 integer -> i16 integer
> >
> > Regards,
> >
> > Denis Berthod
> >
> >
> > Le 26/09/2011 13:42, Jocelyn Sérot a é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<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
> >


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