From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!not-for-mail From: Noah Lavine Newsgroups: gmane.lisp.guile.devel Subject: Re: Some guile-unify activities Date: Fri, 6 May 2011 17:26:41 -0400 Message-ID: References: NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: dough.gmane.org 1304717211 27821 80.91.229.12 (6 May 2011 21:26:51 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Fri, 6 May 2011 21:26:51 +0000 (UTC) Cc: guile-devel To: Stefan Israelsson Tampe Original-X-From: guile-devel-bounces+guile-devel=m.gmane.org@gnu.org Fri May 06 23:26:47 2011 Return-path: Envelope-to: guile-devel@m.gmane.org Original-Received: from lists.gnu.org ([140.186.70.17]) by lo.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1QISXu-0006jl-JK for guile-devel@m.gmane.org; Fri, 06 May 2011 23:26:46 +0200 Original-Received: from localhost ([::1]:49257 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1QISXu-0004dC-1i for guile-devel@m.gmane.org; Fri, 06 May 2011 17:26:46 -0400 Original-Received: from eggs.gnu.org ([140.186.70.92]:55741) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1QISXr-0004d7-5y for guile-devel@gnu.org; Fri, 06 May 2011 17:26:44 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1QISXq-0004vH-0P for guile-devel@gnu.org; Fri, 06 May 2011 17:26:43 -0400 Original-Received: from mail-vx0-f169.google.com ([209.85.220.169]:46011) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1QISXp-0004vD-S1 for guile-devel@gnu.org; Fri, 06 May 2011 17:26:41 -0400 Original-Received: by vxk20 with SMTP id 20so5095941vxk.0 for ; Fri, 06 May 2011 14:26:41 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:cc:content-type :content-transfer-encoding; bh=4ll/8RsG9J/8FnSBvsx2bcf6bD46IXelJ12qHJMABp0=; b=kVW/rkfyNWl6JUXKTM1rumq17UZ04DDqACddjQqu0+3hABRAWaKz5wc7q86+2S6pXH N3nlsi8WtCaz3c5WmSn3mYzFEfWYBCuf6y8mXj7OBfEREhwTnzewdkpz/dhKYFzCg5Mu Hudt7Z2mQHboB4f1F5wp1XVKBuv1oTaN5xUp8= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:cc:content-type :content-transfer-encoding; b=SBkgHxUYEwpwqjKKGNS3ik9D9Pvo5vXEJ7lxHtNmVINOEbL8boRLpiduqo5F3kBxGL K5ywZiI4oZOduCqwH9DCZ3X9Dq4C9+3sTyE1sBPCjL8zmWDjiGvjPMU0xVT7GQjysxUt EcaxbVzW7y9Zp4Ojr289kInt5EViE5BFDJmMA= Original-Received: by 10.52.73.66 with SMTP id j2mr1569196vdv.218.1304717201157; Fri, 06 May 2011 14:26:41 -0700 (PDT) Original-Received: by 10.52.163.5 with HTTP; Fri, 6 May 2011 14:26:41 -0700 (PDT) In-Reply-To: X-Google-Sender-Auth: _YqP_3Jj4APaRsnUGBO04En1CpA X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.6 (newer, 2) X-Received-From: 209.85.220.169 X-BeenThere: guile-devel@gnu.org X-Mailman-Version: 2.1.14 Precedence: list List-Id: "Developers list for Guile, the GNU extensibility library" List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guile-devel-bounces+guile-devel=m.gmane.org@gnu.org Original-Sender: guile-devel-bounces+guile-devel=m.gmane.org@gnu.org Xref: news.gmane.org gmane.lisp.guile.devel:12448 Archived-At: Cool! On Fri, May 6, 2011 at 5:18 PM, Stefan Israelsson Tampe wrote: > Hi, > > Just wanted to chime in and tell you a little about what I'm doing with t= he > guile-unify package. > > First off, this is a tool to do backtracking effectively e.g. tree search= es > and make heavy use of > dynamic variables. > > There is three activities ongoing. > > 1.=A0 type-checking examples > 2.=A0 first order logic solvers (porting leanCop) > 3. documentation > > 1. Documentation, I needed to recap somethings and started to improve on = the > examples above in order to achieve > higher generality. As it turned out bug's in the underlying code is squas= hed > all the time and new useful features for the > macro package is dicoverwed. So the codebase is in a pretty fluent state > still. On the other hand some of the basic features > is being documented. > > 2. The core part of the first order logic leanCop solver has been transla= ted > to a macro package and are now in a pure scheme form. It's not that > advanced. Then there is a language for how to state the problem especiall= y a > translational tool to gather information from a > database of first order logic problems. The idea now is to mod that tool > into spitting out a file of of the translation which are working > then call guile and let guile read in that file and process it with the c= ore > solver. The idea is to test out a few alternative solving teqniques > and evaluate their performance for the database. > > 3. For the type-checking examples I've been working with the assumptions = of > having fixed declarations for > lambdas and deduce types for variables and their passage through the syst= em. > The thought is that in the end > one need to allow lambdas to be explicitly typed in order to allow advanc= ed > type-checking and at the same time > avoid infinite recursions. I think that it's not uncommon in Haskell > programming to add type information in order > to guide the type checker and being at such an infant stage having someth= ing > useful and working must simple allow > for type hint's in the code. > > > It would be cool to let emacs interact with guile to give a tool to > automagically construct > type signatures aka > (lambda (A) B)=A0 > --> (lambda (integer) integer) > > E.g. be able to interactively deduce a type signature. > > I will try to add more type primitives like recursive types and so on to = be > able to match Haskel and typed racket. > Generally the biggest problem with backtracking is complexity issues. One > can design relatively small programs > that makes the type checker work for ages. i will not adress this right n= ow > but there are plenty of short cut's to be taken > in order to speed up the checker. > > It would be good if there was a standard way to enter type information in > guile and if that information could be hooked into the > tree-il representation. But until then I will just use a simple macro > framework to enter typed functions. > > To note below if a lambda produces (or a b) then the rest of the code has= to > be tried with a and when checked then backtrack and be tried with b > if both are type checked then we can proceed. (this is the naive and simp= le > implementation)=A0 So we can have a general type checker but complexity w= ise > it will be awful. > -------------------------------------------------------------------------= ------------------ > So now this works in 1 sec, > ********************** Code (have a geometric explosion in complexity e.g= . > works like 1000 lines of code) ****************** > (tdefine (f X) > =A0 (type (lambda (boolean) (or integer symbol))=A0=A0=A0 ;; type signatu= re is (type > type-desc code ...) and gives a type hint to the lambda > =A0=A0=A0 (let ((F (lambda (P) > =A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 (type (lambda (boolean) (or in= teger symbol)) > =A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 (if P 1 's))))) > =A0=A0=A0=A0=A0 (F #t) > =A0=A0=A0=A0=A0 (F #t) > =A0=A0=A0=A0=A0 (F #t) > =A0=A0=A0=A0=A0 (F #t) > =A0=A0=A0=A0=A0 (F #t) > =A0=A0=A0=A0=A0 (F #t) > =A0=A0=A0=A0=A0 (F #t) > =A0=A0=A0=A0=A0 (F #t) > =A0=A0=A0=A0=A0 (F #t) > =A0=A0=A0=A0=A0 (F #f)))) > ************************************************** first stage compiled > code=A0 *********************************** > (check (lambda ((#{X\ 10764}# : boolean)) > =A0=A0=A0=A0=A0=A0=A0=A0 : > =A0=A0=A0=A0=A0=A0=A0=A0 (or integer symbol) > =A0=A0=A0=A0=A0=A0=A0=A0 (begin > =A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 (let #{F\ 10770}# (lambda > =A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0= =A0=A0=A0=A0=A0 ((#{P\ 10771}# : boolean)) > =A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0= =A0=A0=A0=A0=A0 : > =A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0= =A0=A0=A0=A0=A0 (or integer symbol) > =A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0= =A0=A0=A0=A0=A0 (begin (if #{P\ 10771}# 1 (quote s)))) > =A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 (begin > =A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 (begin > =A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 (apply #{F\ 10770}# (#t)= ) > =A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 (apply #{F\ 10770}# (#t)= ) > =A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 (apply #{F\ 10770}# (#t)= ) > =A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 (apply #{F\ 10770}# (#t)= ) > =A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 (apply #{F\ 10770}# (#t)= ) > =A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 (apply #{F\ 10770}# (#t)= ) > =A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 (apply #{F\ 10770}# (#t)= ) > =A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 (apply #{F\ 10770}# (#t)= ) > =A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 (apply #{F\ 10770}# (#t)= ) > =A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 (apply #{F\ 10770}# (#f)= ))))))) > ---------------------------------------------------------- > **************************************** Deduced Equation > ******************************* > ((=3D (lambda # language/prolog/typecheck/equationalize.scm:72:2 ()>) > =A0=A0=A0 Tres) > =A0((=3D #{X\ 10764}# boolean) > =A0 (=3D (lambda # language/prolog/typecheck/equationalize.scm:72:2 ()>) > =A0=A0=A0=A0 #{F\ 10770}#) > =A0 ((=3D #{P\ 10771}# boolean) > =A0=A0 (or ((=3D (res #{P\ 10771}#) boolean) > =A0=A0=A0=A0=A0=A0=A0 (=3D (res integer) (or integer symbol))) > =A0=A0=A0=A0=A0=A0 ((=3D (res #{P\ 10771}#) boolean) > =A0=A0=A0=A0=A0=A0=A0 (=3D (res symbol) (or integer symbol))))) > =A0 (=3D (res #{F\ 10770}#) > =A0=A0=A0=A0 (lambda (arg Targ10777) Tres10778)) > =A0 (=3D (res boolean) (arg Targ10777)) > =A0 (=3D (res Tres10778) A10776) > =A0 (=3D (res #{F\ 10770}#) > =A0=A0=A0=A0 (lambda (arg Targ10780) Tres10781)) > =A0 (=3D (res boolean) (arg Targ10780)) > =A0 (=3D (res Tres10781) A10779) > =A0 (=3D (res #{F\ 10770}#) > =A0=A0=A0=A0 (lambda (arg Targ10783) Tres10784)) > =A0 (=3D (res boolean) (arg Targ10783)) > =A0 (=3D (res Tres10784) A10782) > =A0 (=3D (res #{F\ 10770}#) > =A0=A0=A0=A0 (lambda (arg Targ10786) Tres10787)) > =A0 (=3D (res boolean) (arg Targ10786)) > =A0 (=3D (res Tres10787) A10785) > =A0 (=3D (res #{F\ 10770}#) > =A0=A0=A0=A0 (lambda (arg Targ10789) Tres10790)) > =A0 (=3D (res boolean) (arg Targ10789)) > =A0 (=3D (res Tres10790) A10788) > =A0 (=3D (res #{F\ 10770}#) > =A0=A0=A0=A0 (lambda (arg Targ10792) Tres10793)) > =A0 (=3D (res boolean) (arg Targ10792)) > =A0 (=3D (res Tres10793) A10791) > =A0 (=3D (res #{F\ 10770}#) > =A0=A0=A0=A0 (lambda (arg Targ10795) Tres10796)) > =A0 (=3D (res boolean) (arg Targ10795)) > =A0 (=3D (res Tres10796) A10794) > =A0 (=3D (res #{F\ 10770}#) > =A0=A0=A0=A0 (lambda (arg Targ10798) Tres10799)) > =A0 (=3D (res boolean) (arg Targ10798)) > =A0 (=3D (res Tres10799) A10797) > =A0 (=3D (res #{F\ 10770}#) > =A0=A0=A0=A0 (lambda (arg Targ10801) Tres10802)) > =A0 (=3D (res boolean) (arg Targ10801)) > =A0 (=3D (res Tres10802) A10800) > =A0 (=3D (res #{F\ 10770}#) > =A0=A0=A0=A0 (lambda (arg Targ10803) Tres10804)) > =A0 (=3D (res boolean) (arg Targ10803)) > =A0 (=3D (res Tres10804) (or integer symbol)))) > ;;; compiled > /home/stis/stis/src/guile/cache/guile/ccache/2.0-0.S-LE-8/home/stis/stis/= src/guile/module/language/typed-guile/test.scm.go > > ************************************************************* Verdict > defined f : (lambda (arg boolean) (or integer symbol)) > $1 =3D #t > > /Stefan >