From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!not-for-mail From: Stefan Israelsson Tampe Newsgroups: gmane.lisp.guile.devel Subject: Re: The progress of hacking guile and prolog Date: Thu, 4 Nov 2010 18:57:10 +0100 Message-ID: <201011041857.10517.stefan.itampe@gmail.com> References: <201010212223.23822.stefan.itampe@gmail.com> <87bp66q8g5.fsf@gnu.org> NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: Text/Plain; charset="utf-8" Content-Transfer-Encoding: quoted-printable X-Trace: dough.gmane.org 1288893420 16249 80.91.229.12 (4 Nov 2010 17:57:00 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Thu, 4 Nov 2010 17:57:00 +0000 (UTC) To: guile-devel@gnu.org Original-X-From: guile-devel-bounces+guile-devel=m.gmane.org@gnu.org Thu Nov 04 18:56:56 2010 Return-path: Envelope-to: guile-devel@m.gmane.org Original-Received: from lists.gnu.org ([199.232.76.165]) by lo.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1PE43T-0004vw-Ez for guile-devel@m.gmane.org; Thu, 04 Nov 2010 18:56:55 +0100 Original-Received: from localhost ([127.0.0.1]:32910 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.43) id 1PE43T-0007S2-2y for guile-devel@m.gmane.org; Thu, 04 Nov 2010 13:56:55 -0400 Original-Received: from [140.186.70.92] (port=37230 helo=eggs.gnu.org) by lists.gnu.org with esmtp (Exim 4.43) id 1PE43P-0007Rl-FF for guile-devel@gnu.org; Thu, 04 Nov 2010 13:56:52 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1PE43O-0002Dq-8P for guile-devel@gnu.org; Thu, 04 Nov 2010 13:56:51 -0400 Original-Received: from mail-ew0-f41.google.com ([209.85.215.41]:43803) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1PE43N-0002DK-Sh for guile-devel@gnu.org; Thu, 04 Nov 2010 13:56:50 -0400 Original-Received: by ewy25 with SMTP id 25so1319491ewy.0 for ; Thu, 04 Nov 2010 10:56:48 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:received:received:from:to:subject:date :user-agent:references:in-reply-to:mime-version:content-type :content-transfer-encoding:message-id; bh=sBpi39PzMTwGa4oUnzgpJI89AkTDgICCMqPgZRcQbBI=; b=JWhYIuc8vYjE052KXdd84gc9NGgEA/cpbIPOxsmi36Eutigt+5dFuiutu90WTct9jX IZEbXy0NgNTvJV/90zFxZK/q3cXtgJw9/Xkv4IcZBpwF6dCS2dZVwSu23rvb0vlaLwFE CiSrevnply3CNp8bp8xSyQeQCvSsQwFOpDpR8= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=from:to:subject:date:user-agent:references:in-reply-to:mime-version :content-type:content-transfer-encoding:message-id; b=pEojM150mb7pLS3jIE6/bhH/ZMofNKZ/9WZwJ6cRaat6LzDGxtCAjPYfjzfAGv0XKh ZC+VgqSkRnOta6a/pxWr68/5PgFZj0N7Sp3YBBW7W18ImoNwsQg+OCyqc6hiAfHMz+ph msPflZJBE6cus0aJTuyEXipw1P5ObMPSfXV/M= Original-Received: by 10.213.12.197 with SMTP id y5mr930102eby.0.1288893408252; Thu, 04 Nov 2010 10:56:48 -0700 (PDT) Original-Received: from linux-s4gz.localnet (1-1-1-39a.veo.vs.bostream.se [82.182.254.46]) by mx.google.com with ESMTPS id v56sm176966eeh.8.2010.11.04.10.56.45 (version=TLSv1/SSLv3 cipher=RC4-MD5); Thu, 04 Nov 2010 10:56:46 -0700 (PDT) User-Agent: KMail/1.13.5 (Linux/2.6.34.7-0.3-desktop; KDE/4.4.4; x86_64; ; ) In-Reply-To: <87bp66q8g5.fsf@gnu.org> X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.6 (newer, 2) X-BeenThere: guile-devel@gnu.org X-Mailman-Version: 2.1.5 Precedence: list List-Id: "Developers list for Guile, the GNU extensibility library" List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Original-Sender: guile-devel-bounces+guile-devel=m.gmane.org@gnu.org Errors-To: guile-devel-bounces+guile-devel=m.gmane.org@gnu.org Xref: news.gmane.org gmane.lisp.guile.devel:11118 Archived-At: On Thursday, November 04, 2010 12:43:54 am Ludovic Court=C3=A8s wrote: > Hi Stefan, >=20 > Lots of stuff here, which is why I took the time to read it. :-) >=20 > Stefan Israelsson Tampe writes: > > 1. The theorem prover (leanCop) is a nice exercise >=20 > [...] >=20 > > 2. Kanren is a nice way to program like with prolog, >=20 > Great that you=E2=80=99re mentioning them. It looks like there=E2=80=99s= a lot of > interesting work that=E2=80=99s been done around Kanren, such as the =E2= =80=9Ctoy=E2=80=9D type > inference engine and, better, =CE=B1leanTAP. I don=E2=80=99t grok it all= I=E2=80=99m glad > you=E2=80=99re looking at it from a Guile perspective. :-) Yes, but I would like to be more true to it then I am right now. So is it=20 enough to reproduce minikanren? Also I've reading in on racklog so I guess what I have right now is correct conceptually but not syntactically. But of cause this can be fixed. So If you think it is worthwhile I will download t= he minikanren sorce hack on. > > 4. The umatch hackity hack was turned into a much more hygienic creatur= e. >=20 > Funny sentence. :-) Well I have two versions one based on the match-phd and is not touching gui= les=20 internals and is based on passing continuations closures and has the proper= ty=20 that all calls are tail calls for basic prolog usage patterns. Also note th= at this principle is not as expensive that one may think if you take into acou= nt=20 a system that inline functions acording to findings from profiling. So in=20 principle all this pushing parameters to the heap could be mitigated. The=20 other one is the hackety hack that tend to be fast on the vm. > > 5) Typechecking is for safty and optimisation, in the end it can be cool > > to have and I'm working to understand all sides of this and have a > > pretty good idea what is needed. It will be a goos testcase for the > > code. >=20 > Yes, if the type inference engine that comes with Kanren could somehow > be hooked into Guile=E2=80=99s compiler, so that it can emit type-mismatch > warnings or determine whether type-checks can be optimized away (which > would require changes in the VM), that=E2=80=99d be great. Notes. 1. It's when compilers start to work you will gain from removing=20 type checks. It's probably not worth it in vm land 2. If a function is used like (f 0.1) in function g and you recompile function f to just allow only fixnums you may end up with havoc. So=20 either function dependencies is tracked or you use the racket way of=20 executing code if going down this optimizing path in a safe way. 3. Of cause local entities can be tracked and optimized away and maybe we should stick to only that. > What=E2=80=99s amazing is that Kanren + type-inference.scm weigh in at = =E2=80=9Conly=E2=80=9D > ~3,500 SLOC. Hence is a powerful concept :-) Hmm I'm also keen to match what typed racket does. I will look into this. > > 6) I copied the glil->assembly compiler and modded the code to spit out > > c-code in stead of assembly. For functions which does not call other > > scheme functions except in tail call manner this should be quite fast to > > adapt. And of cause loops becomes wickedly fast when compiling this way. > > Wingo:s example without consing tok 7ns for each loop on my machine. >=20 > Interesting. Is it a sufficiently isolated change that you could point > us to? Uhmm, I was just curious to se what the overhead of dispatching=20 instructions in a goto-loop would give when I did it. But just think of it as a tool that just inline the c-code behind some simple vm instructions in= =20 stead of the actual vm-instructions. Actually all prolog vanilla prolog=20 code should be able to be compiled quite effectively this way cause it's=20 all tail calls. I'm not sure my code is that interesting though Probably th= e=20 idea is more interesting and should be discussed. The basic idea is to pair the c-code generation with the glil->assembly code so that the compiling function and all it's internal lambda get's corresponding c-function quite automagically and then be gcc:d into linkable code and hooked int these=20 functions vm part that now just act like a trampoline into C land.=20 Do you see it? Have fun Stefan