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 p8REDtOj020002 for ; Tue, 27 Sep 2011 16:13:55 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgkCAFPZgU7AbSoIe2dsb2JhbABBhGSjGBQBARYmBCKBUwEBBSMECwEhJRALCQ8CAiYCAhQYMS6HX6c+kWcOgR6ETjFgBIxQmDg X-IronPort-AV: E=Sophos;i="4.68,449,1312149600"; d="scan'208";a="110768916" Received: from einhorn.in-berlin.de ([192.109.42.8]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 27 Sep 2011 16:13:49 +0200 X-Envelope-From: oliver@first.in-berlin.de Received: from first (e178026150.adsl.alicedsl.de [85.178.26.150]) (authenticated bits=0) by einhorn.in-berlin.de (8.13.6/8.13.6/Debian-1) with ESMTP id p8REDmnD002975; Tue, 27 Sep 2011 16:13:48 +0200 Received: by first (Postfix, from userid 1000) id 3072515404EE; Tue, 27 Sep 2011 16:13:48 +0200 (CEST) Date: Tue, 27 Sep 2011 16:13:48 +0200 From: oliver To: Jocelyn =?utf-8?B?U8Opcm90?= Cc: OCaML Mailing List Message-ID: <20110927141347.GA2837@siouxsie> References: <10F5DBD5-5387-408C-967B-50B37367A6E1@lasmea.univ-bpclermont.fr> <4E806C6F.5050407@gmail.com> <4FAB50A9-43BE-402D-8420-524573F10668@lasmea.univ-bpclermont.fr> <62D492AB-ABD5-4A66-BE41-6191D5813AA5@lasmea.univ-bpclermont.fr> MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Disposition: inline Content-Transfer-Encoding: 8bit In-Reply-To: <62D492AB-ABD5-4A66-BE41-6191D5813AA5@lasmea.univ-bpclermont.fr> User-Agent: Mutt/1.5.20 (2009-06-14) X-Scanned-By: MIMEDefang_at_IN-Berlin_e.V. on 192.109.42.8 Subject: Re: [Caml-list] Dependent types ? 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` (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. > > 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