[Caml-list] Dependent types ?

[Caml-list] Dependent types ?

[Jocelyn Sérot]

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> ...

  

Re: [Caml-list] Dependent types ?

[Thomas Braibant]

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
>
>

Re: [Caml-list] Dependent types ?

[Denis Berthod]

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> ...
>
>
>

Re: [Caml-list] Dependent types ?

[Yaron Minsky]

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

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> 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: 4786 bytes --]

Re: [Caml-list] Dependent types ?

[Denis Berthod]

[-- 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 --]

Re: [Caml-list] Dependent types ?

[Jocelyn Sérot]

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

Thanks to all for your answers.

Phantom types could be a solution but we must declare a new type for  
each possible size, which is cumbersome / annoying.

Moreover, since i'm writing a DSL, the fact that they do not require a  
modification to the existing type system is not really an advantage.
My language has its own type system (largely inspired from OCaml's) so  
what I was looking for was more a way to modify the type  
representation to support the requested behavior.

To those familiar with Caml compiler source code, i was wondering if i  
could hack the following definitions (from types. ml)

type typ =
    | TyVar of typ_var
    | TyTerm of string * typ list

and typ_var =
   { mutable level: int;
     mutable value: tyvar_value }

and tyvar_value =
   | Unknown
   | Known of typ

by adding a notion of "size variable" (sorry if this sounds imprecise,  
this is still a but hazy in my mind..)

type typ =
    | TyVar of typ_var
    | TyTerm of string * typ list * typ_size

and typ_sz =
   { mutable value: tysz_value }

and tyvar_value =
   | Unknown
   | Known of int

and update the unification engine accordingly..

Well, the easiest answer is maybe just to try :-S
I'm just a bit surprised that no one seems to have proposed such an  
extension yet.

Jocelyn

Le 26 sept. 11 à 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>  
> 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: 9437 bytes --]

Re: [Caml-list] Dependent types ?

[Gabriel Scherer]

> Phantom types could be a solution but we must declare a new type for
> each possible size, which is cumbersome / annoying.

If you define the type system yourself, you can easily add a family of
type constants `size<n>` (with `n` an integer literal) to the default
environment of the type checker. Then you can define a parametrized
type `type 's sized_int` (or float, etc.) and instantiate it with any
of the size<n>.

One issue with this minimal -- in term of modifications -- mechanism
is that you can represent meaningless types such as `float size_int` :
`float` is not a size. The canonical way to handle this is to add
a kind system on top of your type system, that would classify the
types into different kinds. Usual types would have kind `★`, and sizes
would have kind `Size`. You would then restrict the `'a` type variable in
`sized_int` to be of kind `Size`:

  type ('a : Size) sized_int

http://en.wikipedia.org/wiki/Kind_(type_theory)

Remark: There is another useful way to combine kinds and sizes, which
is to use "sized kinds" to classify types whose memory representation
has a given size in your implementation. For example you would have
a kind `★` for types of one machine word, `★2` for two machine
words... This allows to keep parametric polymorphism in presence of
non-uniform representations, but it is restricted, less general, as
a given polymorphic definition would not quantify over all types, but
on all types of a given kind – unless you introduce kind polymorphism,
etc. It may be useful for typing low-level programs, but it doesn't
look like what you're looking for here.


On Mon, Sep 26, 2011 at 5:55 PM, Jocelyn Sérot
<Jocelyn.SEROT@ubpmes.univ-bpclermont.fr> wrote:
> Thanks to all for your answers.
> Phantom types could be a solution but we must declare a new type for each
> possible size, which is cumbersome / annoying.
> Moreover, since i'm writing a DSL, the fact that they do not require a
> modification to the existing type system is not really an advantage.
> My language has its own type system (largely inspired from OCaml's) so what
> I was looking for was more a way to modify the type representation to
> support the requested behavior.
> To those familiar with Caml compiler source code, i was wondering if i could
> hack the following definitions (from types. ml)
> type typ =
>    | TyVar of typ_var
>    | TyTerm of string * typ list
> and typ_var =
>   { mutable level: int;
>     mutable value: tyvar_value }
> and tyvar_value =
>   | Unknown
>   | Known of typ
> by adding a notion of "size variable" (sorry if this sounds imprecise, this
> is still a but hazy in my mind..)
> type typ =
>    | TyVar of typ_var
>    | TyTerm of string * typ list * typ_size
> and typ_sz =
>   { mutable value: tysz_value }
> and tyvar_value =
>   | Unknown
>   | Known of int
> and update the unification engine accordingly..
> Well, the easiest answer is maybe just to try :-S
> I'm just a bit surprised that no one seems to have proposed such an
> extension yet.
> Jocelyn
> Le 26 sept. 11 à 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> 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
>>
>
>

Re: [Caml-list] Dependent types ?

[Christophe Raffalli]

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

Hello,

Le 26/09/11 18:44, Gabriel Scherer a écrit :
>> Phantom types could be a solution but we must declare a new type for
>> each possible size, which is cumbersome / annoying.
> If you define the type system yourself, you can easily add a family of
> type constants `size<n>` (with `n` an integer literal) to the default
> environment of the type checker. Then you can define a parametrized
> type `type 's sized_int` (or float, etc.) and instantiate it with any
> of the size<n>.
Another issue is if you wand function additionning size like

concat : int<n> -> int<m> -> int<n+m> (or multiplication)

and zext : int<n> -> int<m> (when m > n)

Then your type system is likely to have to solve problems in Pressburger
arithmetics.
Even only with existential quantifications, this is still not trivial
(no elimination of quantifiers).

But you could probably reuse the code of the Coq Omega tactics ... Or
some other library
like Facile, if you accept limited ranges for you sizes.

I always wanted something like that for size of arrays in OCaml ...

If you have no addition, then this is much easier... and if you have
multiplication, this is likely to be undecidable
(diophantian equations ...).

So you should first list the functions you want with their types ...

Regards,
Christophe

Which is decidable, but not trivial ...



>
> One issue with this minimal -- in term of modifications -- mechanism
> is that you can represent meaningless types such as `float size_int` :
> `float` is not a size. The canonical way to handle this is to add
> a kind system on top of your type system, that would classify the
> types into different kinds. Usual types would have kind `★`, and sizes
> would have kind `Size`. You would then restrict the `'a` type variable in
> `sized_int` to be of kind `Size`:
>
>   type ('a : Size) sized_int
>
> http://en.wikipedia.org/wiki/Kind_(type_theory)
>
> Remark: There is another useful way to combine kinds and sizes, which
> is to use "sized kinds" to classify types whose memory representation
> has a given size in your implementation. For example you would have
> a kind `★` for types of one machine word, `★2` for two machine
> words... This allows to keep parametric polymorphism in presence of
> non-uniform representations, but it is restricted, less general, as
> a given polymorphic definition would not quantify over all types, but
> on all types of a given kind – unless you introduce kind polymorphism,
> etc. It may be useful for typing low-level programs, but it doesn't
> look like what you're looking for here.
>
>
> On Mon, Sep 26, 2011 at 5:55 PM, Jocelyn Sérot
> <Jocelyn.SEROT@ubpmes.univ-bpclermont.fr> wrote:
>> Thanks to all for your answers.
>> Phantom types could be a solution but we must declare a new type for each
>> possible size, which is cumbersome / annoying.
>> Moreover, since i'm writing a DSL, the fact that they do not require a
>> modification to the existing type system is not really an advantage.
>> My language has its own type system (largely inspired from OCaml's) so what
>> I was looking for was more a way to modify the type representation to
>> support the requested behavior.
>> To those familiar with Caml compiler source code, i was wondering if i could
>> hack the following definitions (from types. ml)
>> type typ =
>>    | TyVar of typ_var
>>    | TyTerm of string * typ list
>> and typ_var =
>>   { mutable level: int;
>>     mutable value: tyvar_value }
>> and tyvar_value =
>>   | Unknown
>>   | Known of typ
>> by adding a notion of "size variable" (sorry if this sounds imprecise, this
>> is still a but hazy in my mind..)
>> type typ =
>>    | TyVar of typ_var
>>    | TyTerm of string * typ list * typ_size
>> and typ_sz =
>>   { mutable value: tysz_value }
>> and tyvar_value =
>>   | Unknown
>>   | Known of int
>> and update the unification engine accordingly..
>> Well, the easiest answer is maybe just to try :-S
>> I'm just a bit surprised that no one seems to have proposed such an
>> extension yet.
>> Jocelyn
>> Le 26 sept. 11 à 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> 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
>>>
>>
>


-- 
Christophe Raffalli
Universite de Savoie
Batiment Le Chablais, bureau 21
73376 Le Bourget-du-Lac Cedex

tel: (33) 4 79 75 81 03
fax: (33) 4 79 75 87 42
mail: Christophe.Raffalli@univ-savoie.fr
www: http://www.lama.univ-savoie.fr/~RAFFALLI
---------------------------------------------
IMPORTANT: this mail is signed using PGP/MIME
At least Enigmail/Mozilla, mutt or evolution 
can check this signature. The public key is
stored on www.keyserver.net
---------------------------------------------


[-- Attachment #1.2: Christophe_Raffalli.vcf --]
[-- Type: text/x-vcard, Size: 310 bytes --]

begin:vcard
fn:Christophe Raffalli
n:Raffalli;Christophe
org:LAMA (UMR 5127)
email;internet:christophe.raffalli@univ-savoie.fr
title;quoted-printable:Ma=C3=AEtre de conf=C3=A9rences
tel;work:+33 4 79 75 81 03
note:http://www.lama.univ-savoie.fr/~raffalli
x-mozilla-html:TRUE
version:2.1
end:vcard


[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 250 bytes --]

Re: [Caml-list] Dependent types ?

[oliver]

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

Re: [Caml-list] Dependent types ?

[Jocelyn Sérot]

Le 26 sept. 11 à 18:44, Gabriel Scherer a écrit :

>> Phantom types could be a solution but we must declare a new type for
>> each possible size, which is cumbersome / annoying.
>
> If you define the type system yourself, you can easily add a family of
> type constants `size<n>` (with `n` an integer literal) to the default
> environment of the type checker. Then you can define a parametrized
> type `type 's sized_int` (or float, etc.) and instantiate it with any
> of the size<n>.

Yes. Good point. Thanks for the idea.
IIUC, my add function would be declared as :

val add : 'a sized_int * 'a sized_int -> 'a sized_int

then, with

val x : size16 sized_int
val y : size16 sized_int

the type infered for z in

let z = add (x,y)

will be

z : size16 sized_int

Am i right ?

>
> One issue with this minimal -- in term of modifications -- mechanism
> is that you can represent meaningless types such as `float size_int` :
> `float` is not a size. The canonical way to handle this is to add
> a kind system on top of your type system, that would classify the
> types into different kinds. Usual types would have kind `★`, and  
> sizes
> would have kind `Size`. You would then restrict the `'a` type  
> variable in
> `sized_int` to be of kind `Size`:
>
>  type ('a : Size) sized_int
>
> http://en.wikipedia.org/wiki/Kind_(type_theory)
>
> Remark: There is another useful way to combine kinds and sizes, which
> is to use "sized kinds" to classify types whose memory representation
> has a given size in your implementation. For example you would have
> a kind `★` for types of one machine word, `★2` for two machine
> words... This allows to keep parametric polymorphism in presence of
> non-uniform representations, but it is restricted, less general, as
> a given polymorphic definition would not quantify over all types, but
> on all types of a given kind – unless you introduce kind  
> polymorphism,
> etc. It may be useful for typing low-level programs, but it doesn't
> look like what you're looking for here.

Thanks for the pointer. I'll have a look at this.
But i'm afraid that this would require a too profound change in the  
implementation of the type system..

Jocelyn

>
>
> On Mon, Sep 26, 2011 at 5:55 PM, Jocelyn Sérot
> <Jocelyn.SEROT@ubpmes.univ-bpclermont.fr> wrote:
>> Thanks to all for your answers.
>> Phantom types could be a solution but we must declare a new type  
>> for each
>> possible size, which is cumbersome / annoying.
>> Moreover, since i'm writing a DSL, the fact that they do not  
>> require a
>> modification to the existing type system is not really an advantage.
>> My language has its own type system (largely inspired from OCaml's)  
>> so what
>> I was looking for was more a way to modify the type representation to
>> support the requested behavior.
>> To those familiar with Caml compiler source code, i was wondering  
>> if i could
>> hack the following definitions (from types. ml)
>> type typ =
>>    | TyVar of typ_var
>>    | TyTerm of string * typ list
>> and typ_var =
>>   { mutable level: int;
>>     mutable value: tyvar_value }
>> and tyvar_value =
>>   | Unknown
>>   | Known of typ
>> by adding a notion of "size variable" (sorry if this sounds  
>> imprecise, this
>> is still a but hazy in my mind..)
>> type typ =
>>    | TyVar of typ_var
>>    | TyTerm of string * typ list * typ_size
>> and typ_sz =
>>   { mutable value: tysz_value }
>> and tyvar_value =
>>   | Unknown
>>   | Known of int
>> and update the unification engine accordingly..
>> Well, the easiest answer is maybe just to try :-S
>> I'm just a bit surprised that no one seems to have proposed such an
>> extension yet.
>> Jocelyn
>> Le 26 sept. 11 à 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>  
>> 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
>>>
>>
>>

Re: [Caml-list] Dependent types ?

[Jocelyn Sérot]

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


Le 26 sept. 11 à 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.
>

In the current situation, this will be handled at the VHDL level.
Making it explicit at CAPH (the source level DSL) would be great but  
i'm afraid it is too complex to implement for the moment.
> 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>  
> 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: 5277 bytes --]

Re: [Caml-list] Dependent types ?

[Jocelyn Sérot]

You're perfectly right Christophe,

I now realize that i've opened some kind of Pandora box.

Supporting function declaration

> concat : int<n> -> int<m> -> int<n+m> (or multiplication)

would be great  (even with only addition on sizes), but a too long  
term goal for me (esp. taking into account that i'm by no means a  
specialist in type theory !).

So, a simple approximation like

add : int<n> -> int<n> -> int<n>

(in which the size considerations are supposed to be handled at the  
VHDL level)

would be anough for me..

Jocelyn


Le 26 sept. 11 à 23:09, Christophe Raffalli a écrit :

> Hello,
>
> Le 26/09/11 18:44, Gabriel Scherer a écrit :
>>> Phantom types could be a solution but we must declare a new type for
>>> each possible size, which is cumbersome / annoying.
>> If you define the type system yourself, you can easily add a family  
>> of
>> type constants `size<n>` (with `n` an integer literal) to the default
>> environment of the type checker. Then you can define a parametrized
>> type `type 's sized_int` (or float, etc.) and instantiate it with any
>> of the size<n>.
> Another issue is if you wand function additionning size like
>
> concat : int<n> -> int<m> -> int<n+m> (or multiplication)
>
> and zext : int<n> -> int<m> (when m > n)
>
> Then your type system is likely to have to solve problems in  
> Pressburger
> arithmetics.
> Even only with existential quantifications, this is still not trivial
> (no elimination of quantifiers).
>
> But you could probably reuse the code of the Coq Omega tactics ... Or
> some other library
> like Facile, if you accept limited ranges for you sizes.
>
> I always wanted something like that for size of arrays in OCaml ...
>
> If you have no addition, then this is much easier... and if you have
> multiplication, this is likely to be undecidable
> (diophantian equations ...).
>
> So you should first list the functions you want with their types ...
>
> Regards,
> Christophe
>
> Which is decidable, but not trivial ...
>
>
>
>>
>> One issue with this minimal -- in term of modifications -- mechanism
>> is that you can represent meaningless types such as `float  
>> size_int` :
>> `float` is not a size. The canonical way to handle this is to add
>> a kind system on top of your type system, that would classify the
>> types into different kinds. Usual types would have kind `★`, and  
>> sizes
>> would have kind `Size`. You would then restrict the `'a` type  
>> variable in
>> `sized_int` to be of kind `Size`:
>>
>>  type ('a : Size) sized_int
>>
>> http://en.wikipedia.org/wiki/Kind_(type_theory)
>>
>> Remark: There is another useful way to combine kinds and sizes, which
>> is to use "sized kinds" to classify types whose memory representation
>> has a given size in your implementation. For example you would have
>> a kind `★` for types of one machine word, `★2` for two machine
>> words... This allows to keep parametric polymorphism in presence of
>> non-uniform representations, but it is restricted, less general, as
>> a given polymorphic definition would not quantify over all types, but
>> on all types of a given kind – unless you introduce kind  
>> polymorphism,
>> etc. It may be useful for typing low-level programs, but it doesn't
>> look like what you're looking for here.
>>
>>
>> On Mon, Sep 26, 2011 at 5:55 PM, Jocelyn Sérot
>> <Jocelyn.SEROT@ubpmes.univ-bpclermont.fr> wrote:
>>> Thanks to all for your answers.
>>> Phantom types could be a solution but we must declare a new type  
>>> for each
>>> possible size, which is cumbersome / annoying.
>>> Moreover, since i'm writing a DSL, the fact that they do not  
>>> require a
>>> modification to the existing type system is not really an advantage.
>>> My language has its own type system (largely inspired from  
>>> OCaml's) so what
>>> I was looking for was more a way to modify the type representation  
>>> to
>>> support the requested behavior.
>>> To those familiar with Caml compiler source code, i was wondering  
>>> if i could
>>> hack the following definitions (from types. ml)
>>> type typ =
>>>   | TyVar of typ_var
>>>   | TyTerm of string * typ list
>>> and typ_var =
>>>  { mutable level: int;
>>>    mutable value: tyvar_value }
>>> and tyvar_value =
>>>  | Unknown
>>>  | Known of typ
>>> by adding a notion of "size variable" (sorry if this sounds  
>>> imprecise, this
>>> is still a but hazy in my mind..)
>>> type typ =
>>>   | TyVar of typ_var
>>>   | TyTerm of string * typ list * typ_size
>>> and typ_sz =
>>>  { mutable value: tysz_value }
>>> and tyvar_value =
>>>  | Unknown
>>>  | Known of int
>>> and update the unification engine accordingly..
>>> Well, the easiest answer is maybe just to try :-S
>>> I'm just a bit surprised that no one seems to have proposed such an
>>> extension yet.
>>> Jocelyn
>>> Le 26 sept. 11 à 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>  
>>> 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
>>>>
>>>
>>
>
>
> -- 
> Christophe Raffalli
> Universite de Savoie
> Batiment Le Chablais, bureau 21
> 73376 Le Bourget-du-Lac Cedex
>
> tel: (33) 4 79 75 81 03
> fax: (33) 4 79 75 87 42
> mail: Christophe.Raffalli@univ-savoie.fr
> www: http://www.lama.univ-savoie.fr/~RAFFALLI
> ---------------------------------------------
> IMPORTANT: this mail is signed using PGP/MIME
> At least Enigmail/Mozilla, mutt or evolution
> can check this signature. The public key is
> stored on www.keyserver.net
> ---------------------------------------------
>
> <Christophe_Raffalli.vcf>

Re: [Caml-list] Dependent types ?

[Gabriel Scherer]

> IIUC, my add function would be declared as :
>   val add : 'a sized_int * 'a sized_int -> 'a sized_int
> then, with
>   val x : size16 sized_int
>   val y : size16 sized_int
> the type infered for z in
>   let z = add (x,y)
> will be
>   z : size16 sized_int
>
> Am i right ?

Yes, this is right. You can already experiment in ocaml, as Denis
Berthod suggested, by adding abstract types by hand instead of having
constants in the initial environment.

> You're perfectly right Christophe,
> I now realize that i've opened some kind of Pandora box.
> Supporting function declaration
>   concat : int<n> -> int<m> -> int<n+m> (or multiplication)
> would be great  (even with only addition on sizes), but a too long term goal for me
> (esp. taking into account that i'm by no means a specialist in type theory !).

I think your low-cost approach is reasonable. If you wish to go
further, you could look into Dependent ML, which explored using types
dependent on integers and other kind of data restricted to decidable
constraint domains (presburger arithmetic, etc.), integrating a
domain-specific solver in the type system.
  http://www.cs.bu.edu/~hwxi/DML/DML.html
Hongwei Xi is now working on ATS, which reuses those ideas and goes
further, aiming at statically safe low-level programming, but in a
more complex framework
  http://www.ats-lang.org/
Also related is the currently ongoing design of the Habit language,
which also uses restricted arithmetic operations at the type level.
  http://hasp.cs.pdx.edu/

On Tue, Sep 27, 2011 at 10:23 AM, Jocelyn Sérot
<Jocelyn.SEROT@ubpmes.univ-bpclermont.fr> wrote:
>
> Le 26 sept. 11 à 18:44, Gabriel Scherer a écrit :
>
>>> Phantom types could be a solution but we must declare a new type for
>>> each possible size, which is cumbersome / annoying.
>>
>> If you define the type system yourself, you can easily add a family of
>> type constants `size<n>` (with `n` an integer literal) to the default
>> environment of the type checker. Then you can define a parametrized
>> type `type 's sized_int` (or float, etc.) and instantiate it with any
>> of the size<n>.
>
> Yes. Good point. Thanks for the idea.
> IIUC, my add function would be declared as :
>
> val add : 'a sized_int * 'a sized_int -> 'a sized_int
>
> then, with
>
> val x : size16 sized_int
> val y : size16 sized_int
>
> the type infered for z in
>
> let z = add (x,y)
>
> will be
>
> z : size16 sized_int
>
> Am i right ?
>
>>
>> One issue with this minimal -- in term of modifications -- mechanism
>> is that you can represent meaningless types such as `float size_int` :
>> `float` is not a size. The canonical way to handle this is to add
>> a kind system on top of your type system, that would classify the
>> types into different kinds. Usual types would have kind `★`, and sizes
>> would have kind `Size`. You would then restrict the `'a` type variable in
>> `sized_int` to be of kind `Size`:
>>
>>  type ('a : Size) sized_int
>>
>> http://en.wikipedia.org/wiki/Kind_(type_theory)
>>
>> Remark: There is another useful way to combine kinds and sizes, which
>> is to use "sized kinds" to classify types whose memory representation
>> has a given size in your implementation. For example you would have
>> a kind `★` for types of one machine word, `★2` for two machine
>> words... This allows to keep parametric polymorphism in presence of
>> non-uniform representations, but it is restricted, less general, as
>> a given polymorphic definition would not quantify over all types, but
>> on all types of a given kind – unless you introduce kind polymorphism,
>> etc. It may be useful for typing low-level programs, but it doesn't
>> look like what you're looking for here.
>
> Thanks for the pointer. I'll have a look at this.
> But i'm afraid that this would require a too profound change in the
> implementation of the type system..
>
> Jocelyn
>
>>
>>
>> On Mon, Sep 26, 2011 at 5:55 PM, Jocelyn Sérot
>> <Jocelyn.SEROT@ubpmes.univ-bpclermont.fr> wrote:
>>>
>>> Thanks to all for your answers.
>>> Phantom types could be a solution but we must declare a new type for each
>>> possible size, which is cumbersome / annoying.
>>> Moreover, since i'm writing a DSL, the fact that they do not require a
>>> modification to the existing type system is not really an advantage.
>>> My language has its own type system (largely inspired from OCaml's) so
>>> what
>>> I was looking for was more a way to modify the type representation to
>>> support the requested behavior.
>>> To those familiar with Caml compiler source code, i was wondering if i
>>> could
>>> hack the following definitions (from types. ml)
>>> type typ =
>>>   | TyVar of typ_var
>>>   | TyTerm of string * typ list
>>> and typ_var =
>>>  { mutable level: int;
>>>    mutable value: tyvar_value }
>>> and tyvar_value =
>>>  | Unknown
>>>  | Known of typ
>>> by adding a notion of "size variable" (sorry if this sounds imprecise,
>>> this
>>> is still a but hazy in my mind..)
>>> type typ =
>>>   | TyVar of typ_var
>>>   | TyTerm of string * typ list * typ_size
>>> and typ_sz =
>>>  { mutable value: tysz_value }
>>> and tyvar_value =
>>>  | Unknown
>>>  | Known of int
>>> and update the unification engine accordingly..
>>> Well, the easiest answer is maybe just to try :-S
>>> I'm just a bit surprised that no one seems to have proposed such an
>>> extension yet.
>>> Jocelyn
>>> Le 26 sept. 11 à 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> 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
>>>>
>>>
>>>
>
>
>
> --
> 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
>
>

Re: [Caml-list] Dependent types ?

[Arnaud Spiwack]

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

> Yes, this is right. You can already experiment in ocaml, as Denis
> Berthod suggested, by adding abstract types by hand instead of having
> constants in the initial environment.
>

You can also embed the natural numbers in Ocaml's type system by declaring
the following two types:

type 'a s
type z

Granted 32 would be written z s s s s s s s s s s s s s s s s s s s s s s s
s s s s s s s s s which may or may not be considered legible. But at least
there is no absolute need for infinitely many constants.

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

Re: [Caml-list] Dependent types ?

[Jocelyn Sérot]

Well, clever and funny idea ;-)

But not specially user-friendly, esp. if you take into account the  
fact that the user of my DSL are mainly VHDL programmers, not  
particularly familiar with FP and polymorphic type systems...

Thanks for the idea, anyway

Jocelyn

Le 27 sept. 11 à 11:41, Arnaud Spiwack a écrit :

>
> Yes, this is right. You can already experiment in ocaml, as Denis
> Berthod suggested, by adding abstract types by hand instead of having
> constants in the initial environment.
>
> You can also embed the natural numbers in Ocaml's type system by  
> declaring the following two types:
>
> type 'a s
> type z
>
> Granted 32 would be written z s s s s s s s s s s s s s s s s s s s  
> s s s s s s s s s s s s s which may or may not be considered  
> legible. But at least there is no absolute need for infinitely many  
> constants.

Re: [Caml-list] Dependent types ?

[oliver]

Hello,


On Tue, Sep 27, 2011 at 10:23:56AM +0200, Jocelyn Sérot wrote:
> 
> Le 26 sept. 11 à 18:44, Gabriel Scherer a écrit :
> 
> >>Phantom types could be a solution but we must declare a new type for
> >>each possible size, which is cumbersome / annoying.
> >
> >If you define the type system yourself, you can easily add a family of
> >type constants `size<n>` (with `n` an integer literal) to the default
> >environment of the type checker. Then you can define a parametrized
> >type `type 's sized_int` (or float, etc.) and instantiate it with any
> >of the size<n>.
> 
> Yes. Good point. Thanks for the idea.
> IIUC, my add function would be declared as :
> 
> val add : 'a sized_int * 'a sized_int -> 'a sized_int
> 
> then, with
> 
> val x : size16 sized_int
> val y : size16 sized_int
> 
> the type infered for z in
> 
> let z = add (x,y)
> 
> will be
> 
> z : size16 sized_int
> 
> Am i right ?
[...]

Not sure.

Depends on what you want ;-)

What would the type system
yield fopr a type for



val x : size16 sized_int
val y : size16 sized_int

let z = and_msb (x,y)  # AND the MSBs of both input values

z might be 16 Bits, if this is your "natural" int size - but: what is natural on
FPGA's, when you can change your HW at will?
And: if it's "batural", why to declare it?

But ANDing two Bits will result in a 1 Bit result.

Why should z be 16 Bits then?
That would be wasting ressources.

IMHO it does not make sense to derive the type of z from the type of
x and y. It must be derived from the operation or function that is used.


If you use  'a sized_int   then  this would offer you
the possibility also of taking 2 x 16 Bits and get 1 Bit (as in the and_msb()-example)
but of course also to do your

z = add (x,y) with z of 16 Bits, which you looked for.

But is thats a type that can be derived from x and y?

Or is it rather the OPERATION ("add" here), or better: the operation
together with the input values, that fives you the resulting type?

What if you do:

val x : size16 sized_int
val y : size8  sized_int

z = add(x, y)

What type does z no have?

8 Bits? 16 Bits?
Somewhere in between?


AFAIK one of the biggest (or better: THE) advantage of FPGAs/VHDL is:
you can create your "HW" (HW connections) by SW.

So you are not fixed in width, and you can save some bits here and there,
and use them later somewhere else...


And, I doubt, somehow, that what you are talking about is a "type issue".
At least nothing that can be derived from the structure of the inputs
without knowing the operation.

AFAIK you are not constrained to a fixed ALU and databus width,
at least not in a sense as we know it from fixed HW that we normally use
when buying a computer at the store.
(There may be limits of course, depending on the FPGA device in use.)


So, how do you address these issues?

I would say either you also need to define the type of z,
or you need to derive the type from the source of which
your operations/functions are derived.

So: you need more information than what you presented in your questions,
to decide for the resulting type.

Ciao,
   Oliver

Re: [Caml-list] Dependent types ?

[Denis Berthod]

[-- 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 --]

[Caml-list] Dependent types ?

[Damien Guichard]

[-- 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 --]