From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p2VNm9O4004485 for ; Fri, 1 Apr 2011 01:48:10 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AvgAAN4RlU1V2gB5nGdsb2JhbAClbQEBAQEBCAsJCRQliHm3bA2FXgSRAA X-IronPort-AV: E=Sophos;i="4.63,279,1299452400"; d="scan'208";a="95507889" Received: from emailfrontal2.citycable.ch ([85.218.0.121]) by mail2-smtp-roc.national.inria.fr with SMTP; 01 Apr 2011 01:48:04 +0200 X-Alinto-smtpauth-localdomain: Yes Received: from seldon (unknown [85.218.93.111]) (Authenticated sender: guillaume.yziquel@citycable.ch) by emailfrontal2.citycable.ch (Postfix) with ESMTPA id D0EFB83450E; Fri, 1 Apr 2011 01:48:02 +0200 (CEST) Received: from yziquel by seldon with local (Exim 4.72) (envelope-from ) id 1Q5RZW-0004W3-B2; Fri, 01 Apr 2011 01:46:40 +0200 Date: Fri, 1 Apr 2011 01:46:19 +0200 From: Guillaume Yziquel To: Gabriel Scherer Cc: caml-list@inria.fr Message-ID: <20110331234612.GG10930@localhost> References: <20110330222702.GF20598@localhost> MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Disposition: inline In-Reply-To: User-Agent: Mutt/1.5.20 (2009-06-14) Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id p2VNm9O4004485 Subject: Re: [Caml-list] Reasoning about categories at compile-time. Le Thursday 31 Mar 2011 à 08:02:30 (+0200), Gabriel Scherer a écrit : > First, one obvious solution : parse the equations, run a solver, then > output "()" if it can deduce the queries from the equations, and "1 = > true" otherwise. Why isn't this solution satisfying ? Because that would mean, in Camlp4, doing a processing of the whole module X : sig (* category constraints / proof goals *) end = struct (* category axioms *) end I want to be able to deal separately with .ml and .mli files. Or with a module structure and a module signature. Therefore I need it to be such that it is the type checker that is in charge of being the solver. I'd love a 'type system extension' mechanism... this way I could include the solver in it. > With the type system there is one thing that is easy and natural to do > : you could encode your arrows as elements with a specific type (eg. > for an arrow `f` of source `src` and destination `dst` you would write > `(src, f, dst) arrow` with `src, f, dst` abstract types) : > > arrow_f : (foo, f, bar) arrow > > then write both a composition function > > compose : ('a, 'f, 'b) arrow -> ('b, 'g, 'c) arrow -> ('a, ('f, 'g) comp, 'c) arrow > > and terms representing your equational theory: > > assoc : ('a, (('f, 'g) comp, 'h) comp, 'b) arrow -> ('a, ('f, ('g, 'h) comp) comp, 'b) > > and for each equation f o g = h (not that I use `g` and not `'g`) > > witness_fg_h : ('a, (f, g) comp, 'b) arrow -> ('a, h, 'b) arrow > > Then, for each deducible relation, there exist a typed term that is a > proof witness of the relation deductibility (you just unify the type of > the two arrows that should be equal). If you have a solver for equation > deductibility, you can ask him to output the proof witness in this > format. I thought of that, though not as precisely as you're exposing it. But keeping the .ml / .mli distinction and compiling them separately, you have a problem: Essentially, the witnesses live in the .ml file, and the proof witness also lives in the .ml file. In the .mli file, you simply have to declare the existence of a proof witness term. However, in order to construct the proof witness, you need to know the goal that you wish to prove, which means providing to camlp4 some information that lives in the .mli file. This would break separate compilation. Or rather separate preprocessing. You could not preprocess the .ml file before the .mli file. Worse: you could not do: module X with syntax extension = struct ... end module type S with syntax extension = sig ... end let m = (module X : S) (which is what I want to do, specifically). > This does not use the inference system to solve your problem, which is > what you asked for. But this is a solid design that is going to still > work if you change your language, eg. can still be used on non > decidable questions. I think this is a good first step; feel free to > improve it by whatever advanced type hackery. Unfortunately, this doesn't fit the bill. I had this picture in mind intuitively but not formalised, and I saw the limitation I explained above. That's what prompted me to ask on the list in the first place. But thanks for clarifying my hazy thoughts. What bugs me is that, to put it simply, the category axioms are generated by Camlp4 in a non-deterministic fashion, dependent on the outside world. You only have control in user code on the proof goals. What you propose means linking module struct and module type syntactically. However, I'd need them decoupled as I'd like in the long run to do the following: You have two categories, C1 and C2. You take the set union of both categories C1 U C2. (Set union of objects, and set unions of arrows). This gives two OCaml modules. You include both modules into a bigger module, add some arrows and arrow composition axioms. You then want to match them against a module signature describing the proof goals. Do the same thing with first-class modules (OCaml 3.13 doesn't need so much module signatures as OCaml 3.12 for first-class modules, which goes in the sense of 'decoupling' preprocessed modules and preprocessed signatures), and you get an idea of what I'm up to. That's why I'm looking for a purely type-system encoding of this problem. Somehow lifting the solver for equational deducibility you mentionned into the type inference algo itself. So instead of having arrows as private types, I was thinking of having arrows as type parameters. And have unification doing the solving. Unfortunately, if you put equational constraints in the module signature, they leak into the module implementation (funny to have a signature leaking in an implementation by the way). Just think of the simple module X : sig val f : 'a -> 'a end = struct let f : 'a -> 'b = Obj.magic end This is somehow reversed: module X : sig val f : 'a -> 'b end = struct let f : 'a -> 'a = assert false end fails to type-check, which could perhaps be understood as 'given two types not known to be equal, I fail to conclude that 'a = 'a and 'b = 'a, i.e. I fail to conclude that 'b = 'a. This is tautological, but it's interesting to see that the axioms are now in the signature and the goal in the module structure. I was wondering perhaps naïvely how much truth there is in the above paragraph, and if it could be used to encode the equational solver into the unification algo in one way or another. -- Guillaume Yziquel