From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p8QCjOSq024443 for ; Mon, 26 Sep 2011 14:45:24 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ArMBAJxygE7RVdy2mGdsb2JhbABBmRg1hxoBhx4IFAEBAQEBCAkNBxQmgVMBAQEECwcCEwQVARsSCwEDDAYFCw0NISEBAQwBBAEFAQMBBhIGExIQh1ydQAqLTAqCUoRUO4huAgMGgxKDcwSCVIUci2KGD4QIgnI9OYNB X-IronPort-AV: E=Sophos;i="4.68,444,1312149600"; d="scan'208";a="110547645" Received: from mail-vx0-f182.google.com ([209.85.220.182]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 26 Sep 2011 14:45:18 +0200 Received: by vcbf13 with SMTP id f13so5218668vcb.27 for ; Mon, 26 Sep 2011 05:45:17 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=mime-version:reply-to:in-reply-to:references:date:message-id :subject:from:to:cc:content-type; bh=3dDGWCRer/hymJQ2lDi25+NTJElbhPWYThkpGGVGEUY=; b=n7ZbNdbPdulWvDqktUYq6ASeWJ95YgMKuEgB3SEDB2XF+lc044mLZnJmWnRnBYmMCc V9C/DAqfYjPSHMrL1G352A9Qbnyl3V4u3HOSYQaQCWhMaLmL/a8u/jhOdQMSFNQvh7A7 NjND8CBeyqSGHkwNTZf9cxDTZ3tHsrKwAX0v4= MIME-Version: 1.0 Received: by 10.52.66.38 with SMTP id c6mr6704775vdt.22.1317041117350; Mon, 26 Sep 2011 05:45:17 -0700 (PDT) Received: by 10.220.158.132 with HTTP; Mon, 26 Sep 2011 05:45:16 -0700 (PDT) Received: by 10.220.158.132 with HTTP; Mon, 26 Sep 2011 05:45:16 -0700 (PDT) Reply-To: yminsky@gmail.com In-Reply-To: <4E806C6F.5050407@gmail.com> References: <10F5DBD5-5387-408C-967B-50B37367A6E1@lasmea.univ-bpclermont.fr> <4E806C6F.5050407@gmail.com> Date: Mon, 26 Sep 2011 20:45:16 +0800 Message-ID: From: Yaron Minsky To: Denis Berthod Cc: caml-list@inria.fr Content-Type: multipart/alternative; boundary=20cf3071c9e8f44ac804add78750 Subject: Re: [Caml-list] Dependent types ? --20cf3071c9e8f44ac804add78750 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable 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" 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 > =3D > struct > type 'a integer =3D int > > let int16 x =3D x > let int32 x =3D x > > let add x y =3D x + y > end > > then > > open SizedInt > > let bar =3D > let x =3D int16 42 in > foo x > > must have type i16 integer -> i16 integer > > Regards, > > Denis Berthod > > > Le 26/09/2011 13:42, Jocelyn S=E9rot a =E9crit : >> 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 =3D 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 > --20cf3071c9e8f44ac804add78750 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable

As written, the behavior of the types might not be what you expect, sinc= e 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 typ= es mean what you think they mean.

On Sep 26, 2011 8:13 AM, "Denis Berthod&quo= t; <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/unb= oxing in records.
>
> type i16
> type i32
>
&g= t; module SizedInt:
> sig
> type 'a integer
> val int16: int -> i16 integer
> val int32: in= t -> i32 integer
> val add: 'a integer -> 'a in= teger -> 'a integer
> end
> =3D
> stru= ct
> type 'a integer =3D int
>
> let int= 16 x =3D x
> let int32 x =3D x
>
> let = add x y =3D x + y
> end
>
> then
>
> o= pen SizedInt
>
> let bar =3D
> let x =3D int16 42 in
> foo= x
>
> must have type i16 integer -> i16 integer
> > Regards,
>
> Denis Berthod
>
>
> Le= 26/09/2011 13:42, Jocelyn S=E9rot a =E9crit :
>> Hello,
>>
>> I've recently come across a pro= blem while writing a domain specific
>> language for hardware syn= thesis
>> (http://wwwlasmea.univ-bpclermont.fr/Personnel/J= ocelyn.Serot/caph.html).
>> The idea is to extend the type system to accept "size" a= nnotations for
>> int types (it could equally apply to floats).>> The target language (VHDL in this case) accept "generic&quo= t; functions,
>> operating on ints with variable bit width and I'd like to refl= ect this
>> in the source language.
>>
>> For i= nstance, I'd like to be able to declare :
>>
>> val f= oo : int * int -> int
>>
>> (where the type int is not annotated, i.e. "gener= ic")
>>
>> so that, when applied to, let say :
&g= t;>
>> val x : int<16>
>> val y : int<16><= br> >>
>> (where <16> is a size annotation),
>>>> like in
>>
>> let z =3D foo (x,y)
>><= br>>> then the compiler will infer type int<16> for z
>&g= t;
>> 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 ->= 9;b) -> 'b list).
>>
>> In a sense, it has to do w= ith the theory of sized types (Hughes and
>> Paretto, .. ) and de= pendent types (DML for ex), but my goal is far
>> less ambitious.
>> In particular, i dont want to do _comp= utations_ (1) on the size (and,
>> a fortiori, don't want to = prove anything on the programs).
>> So sized types / dependent typ= es seems a big machinery for a
>> relatively small goal.
>> My intuition is that this is ju= st a variant of polymorphism in which
>> the variables ranged ove= r 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
>>
>> J= ocelyn
>>
>> (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-ro= c.inria.fr/wws/info/caml-list
> Beginner's list: http://groups.yahoo.com/group= /ocaml_beginners
> Bug reports: http://cam= l.inria.fr/bin/caml-bugs
>
--20cf3071c9e8f44ac804add78750--