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 p8QMpJLJ011507
	for <caml-list@sympa-roc.inria.fr>; Tue, 27 Sep 2011 00:51:19 +0200
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AlUCAHkBgU7AbSoIe2dsb2JhbABChGKjDBQBARYmBCKBUwEBBSMECwEhJRALCQ8CAiYCAhQYMYgNBKgWkX4OgR6ETjFgBIxQmDc
X-IronPort-AV: E=Sophos;i="4.68,447,1312149600"; 
   d="scan'208";a="110639183"
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 00:51:14 +0200
X-Envelope-From: oliver@first.in-berlin.de
Received: from first (e178007018.adsl.alicedsl.de [85.178.7.18])
	(authenticated bits=0)
	by einhorn.in-berlin.de (8.13.6/8.13.6/Debian-1) with ESMTP id p8QMpDHR011930;
	Tue, 27 Sep 2011 00:51:13 +0200
Received: by first (Postfix, from userid 1000)
	id 0BC141540137; Tue, 27 Sep 2011 00:51:12 +0200 (CEST)
Date: Tue, 27 Sep 2011 00:51:12 +0200
From: oliver <oliver@first.in-berlin.de>
To: Jocelyn =?utf-8?B?U8Opcm90?= <Jocelyn.SEROT@ubpmes.univ-bpclermont.fr>
Cc: OCaML Mailing List <caml-list@inria.fr>
Message-ID: <20110926225112.GA1727@siouxsie>
References: <10F5DBD5-5387-408C-967B-50B37367A6E1@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: <10F5DBD5-5387-408C-967B-50B37367A6E1@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 ?

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