From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p2V62v77026203 for ; Thu, 31 Mar 2011 08:02:57 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AlEDAD0YlE3RVdivimdsb2JhbACYIoY5AYYaWQgUAQEBCgkNBxIGIYh5mxmKVYIihFAviFwBAQMFhWUEgXuLC4kOOg X-IronPort-AV: E=Sophos;i="4.63,273,1299452400"; d="scan'208";a="79517815" Received: from mail-qy0-f175.google.com ([209.85.216.175]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 31 Mar 2011 08:02:51 +0200 Received: by qyk35 with SMTP id 35so3855406qyk.6 for ; Wed, 30 Mar 2011 23:02:50 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:mime-version:in-reply-to:references:from:date :message-id:subject:to:cc:content-type; bh=LBPBr2+69QikXMYVmywb35nbF854oeqiyvj6DTQ7I+A=; b=BU7hLeiYPAenay1e0GCgHZsZzmCcSeYfF1dHwe8OCt2Tjg373fgPYTa8p4ygVGbSIK aNz4B8jvN028PjzL0FsIiWngsf8HYhzzf/os/FOm+6Al2xXHqRrJ3E2HcvzpOqj1f2bW Zwi/n80Ot7I3ISUB6qO1bK/KgF1vgZTLAqx/o= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; b=AsQOVZASewT2HpeSbFfUVlFsUAR4Cu/FEgnsFFwghFjk186dMCWBltLMX9qioO9jej r1Dmnvx2keK0yboTrsPNikX8PxYf57OfMFLAix6Abfs5S+4aPrebMuJ0cmeR1uDzF86t HQooEd5unmp1/w1Vb6PRZupMZ8sFSY8y2TXqM= Received: by 10.229.221.139 with SMTP id ic11mr1872277qcb.129.1301551370283; Wed, 30 Mar 2011 23:02:50 -0700 (PDT) MIME-Version: 1.0 Received: by 10.229.235.146 with HTTP; Wed, 30 Mar 2011 23:02:30 -0700 (PDT) In-Reply-To: <20110330222702.GF20598@localhost> References: <20110330222702.GF20598@localhost> From: Gabriel Scherer Date: Thu, 31 Mar 2011 08:02:30 +0200 Message-ID: To: Guillaume Yziquel Cc: caml-list@inria.fr Content-Type: multipart/alternative; boundary=001636283a02152ca4049fc10b58 Subject: Re: [Caml-list] Reasoning about categories at compile-time. --001636283a02152ca4049fc10b58 Content-Type: text/plain; charset=ISO-8859-1 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 ? 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. 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. On Thu, Mar 31, 2011 at 12:27 AM, Guillaume Yziquel < guillaume.yziquel@citycable.ch> wrote: > 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 > > -- > 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 > > --001636283a02152ca4049fc10b58 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable First, one obvious solution : parse the equations, run a solver, then outpu= t "()" if it can deduce the queries from the equations, and "= ;1 =3D true" otherwise. Why isn't this solution satisfying ?
With the type system there is one thing that is easy and natural to do : yo= u could encode your arrows as elements with a specific type (eg. for an arr= ow `f` of source `src` and destination `dst` you would write `(src, f, dst)= arrow` with `src, f, dst` abstract types) :
=A0 arrow_f : (foo, f, bar) arrow
then write both a composition function=
=A0 compose : ('a, 'f, 'b) arrow -> ('b, 'g, = 9;c) arrow -> ('a, ('f, 'g) comp, 'c) arrow
and terms= representing your equational theory:
=A0 assoc : ('a, (('f, 'g) comp, 'h) comp, 'b) arrow -&= gt; ('a, ('f, ('g, 'h) comp) comp, 'b)
and for each = equation f o g =3D h (not that I use `g` and not `'g`)
=A0 witness_f= g_h : ('a, (f, g) comp, 'b) arrow -> ('a, h, 'b) arrow
Then, for each deducible relation, there exist a typed term that is a p= roof 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 deducti= bility, you can ask him to output the proof witness in this format.

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 questio= ns. I think this is a good first step; feel free to improve it by whatever = advanced type hackery.

On Thu, Mar 31, 2011 at 12:27 AM, Guillaume = Yziquel <guillaume.yziquel@citycable.ch> wrote:
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<= br> 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

=A0 =A0 =A0 =A0f o g o h =3D i o j o k

and the unprocessed .ml file contains

=A0 =A0 =A0 =A0f o g =3D i
=A0 =A0 =A0 =A0h =3D j o k

I want it to type check fine. I you ommit h =3D 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.

--
=A0 =A0 Guillaume Yziquel

--
Caml-list mailing list. =A0Subscription 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


--001636283a02152ca4049fc10b58--