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 p2UMSUxR002931 for ; Thu, 31 Mar 2011 00:28:30 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AlUGABquk01V2gB4hWdsb2JhbACYU40YAQEBCgsLBRYlvxINhV0EkHU X-IronPort-AV: E=Sophos;i="4.63,270,1299452400"; d="scan'208";a="91566493" Received: from emailfrontal1.citycable.ch ([85.218.0.120]) by mail4-smtp-sop.national.inria.fr with SMTP; 31 Mar 2011 00:28:24 +0200 X-Alinto-smtpauth-localdomain: Yes Received: from seldon (unknown [85.218.93.111]) (Authenticated sender: guillaume.yziquel@citycable.ch) by emailfrontal1.citycable.ch (Postfix) with ESMTPA id 63DCA12C233; Thu, 31 Mar 2011 00:28:18 +0200 (CEST) Received: from yziquel by seldon with local (Exim 4.72) (envelope-from ) id 1Q53qz-0002cS-1W; Thu, 31 Mar 2011 00:27:05 +0200 Date: Thu, 31 Mar 2011 00:27:04 +0200 From: Guillaume Yziquel To: caml-list@inria.fr Message-ID: <20110330222702.GF20598@localhost> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline User-Agent: Mutt/1.5.20 (2009-06-14) Subject: [Caml-list] Reasoning about categories at compile-time. Hello. I have a small problem that I would wish to encode in the type system, and I would like some advice on how to do that using Camlp4. You have a finite category (in the sense of a finite number of objects), and a finite set of arrows that generates all the arrows. Let's assume that you have tokens (Camlp4 a_LIDENT) for all of these. I want my Camlp4 syntax extension to operate on an .mli interface file and an .ml file. The .mli interface should contain all the relations you want to enforce concerning composition of arrows. The .ml file should contain some relations about composition of arrows. If I compile the preprocessed .ml file against the preprocessed .mli file, I want it to type check if and only if all relations in the .mli file can be deduced from relations in the .mli file. If, for instance the unprocessed .mli file contains f o g o h = i o j o k and the unprocessed .ml file contains f o g = i h = j o k I want it to type check fine. I you ommit h = j o k, I want the type checker to fail. This is purely type-system-ish, and I really do not care how arrows are encoded (types, type parameters, fun (type arrow) -> stuff). Is there a way to use Camlp4 to encode this in the type system? Intuitively, I'd say yes, but I currently do not see how. -- Guillaume Yziquel