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: The progress of hacking guile and prolog Date: Wed, 3 Nov 2010 22:40:09 -0400 Message-ID: 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 1288838427 10389 80.91.229.12 (4 Nov 2010 02:40:27 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Thu, 4 Nov 2010 02:40:27 +0000 (UTC) Cc: guile-devel@gnu.org To: =?ISO-8859-1?Q?Ludovic_Court=E8s?= Original-X-From: guile-devel-bounces+guile-devel=m.gmane.org@gnu.org Thu Nov 04 03:40:22 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 1PDpkT-0005IQ-Vh for guile-devel@m.gmane.org; Thu, 04 Nov 2010 03:40:22 +0100 Original-Received: from localhost ([127.0.0.1]:41015 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.43) id 1PDpkT-0003Mc-HS for guile-devel@m.gmane.org; Wed, 03 Nov 2010 22:40:21 -0400 Original-Received: from [140.186.70.92] (port=38008 helo=eggs.gnu.org) by lists.gnu.org with esmtp (Exim 4.43) id 1PDpkM-0003MJ-12 for guile-devel@gnu.org; Wed, 03 Nov 2010 22:40:15 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1PDpkJ-00022V-F9 for guile-devel@gnu.org; Wed, 03 Nov 2010 22:40:13 -0400 Original-Received: from mail-wy0-f169.google.com ([74.125.82.169]:53855) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1PDpkJ-00021p-AW; Wed, 03 Nov 2010 22:40:11 -0400 Original-Received: by wyf23 with SMTP id 23so1545254wyf.0 for ; Wed, 03 Nov 2010 19:40:09 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:mime-version:received:sender:received :in-reply-to:references:date:x-google-sender-auth:message-id:subject :from:to:cc:content-type:content-transfer-encoding; bh=7K63JQXF4/NiBPS18yaQj1V0mF/saRgITo96I6+dw2g=; b=EMV/HFBhQyli1P7tnLMS2feyxhOzfYbdeD5Gn5wsf66HAGd71KFHBU1SBLIs9S1aAS l+qmRYdWqWme7oXCYgib5cMcpjaj/OZEv4RO5Hooi6MKXphBrYOwHkK81MFLhgztvM9I 0uhRKc5LJRNiMXsskY9LeuV3BhZ6Jn6Blne+g= 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=R40+HgS/nA2faU36KXsSfnvLpXuLxhDjQKuzH+N2Rmg620TpTwUtxpzY6dGwzVcKj/ oVJyCrSBcFTFrLrhpZ5mdHP5zkLSriwRtBdjz+1FSmtpHdcInWLRWxOFpYlvQHOSbs1e PCb3jyybeFriUYaaKc06INboH0OcBpvymmNXg= Original-Received: by 10.216.87.20 with SMTP id x20mr1282986wee.52.1288838409331; Wed, 03 Nov 2010 19:40:09 -0700 (PDT) Original-Received: by 10.216.237.34 with HTTP; Wed, 3 Nov 2010 19:40:09 -0700 (PDT) In-Reply-To: <87bp66q8g5.fsf@gnu.org> X-Google-Sender-Auth: 7cW2SkiyEewKVhz19iPlvCed_w4 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:11116 Archived-At: Hello all, Not to derail the thread of discussion, but I've had an idea for a feature bouncing around that I think might hook into this. I think that Guile should offer optional static checking - not just of types, but of everything that we can check. It could be used partly for optimization, but partly also as a way to verify that you're reasoning about the program correctly. (Like assert, but you prove things correct.) For instance, (define (map func list) (check (=3D (arity func) 1)) ....) or (define (search-binary-search-tree tree key) (check (binary-search-tree? tree) ; or whatever conditions make sense ....) I'm afraid I don't know much about how theorem provers like that would be used to make static checkers, but is there a way to use LeanCOP or Kanren to provide something like this? I think the easiest interface would be one where you could put arbitrary Scheme code in check statements, but the prover would be able to reject it as "unable to check this", in which case it could insert a runtime check (if you asked it to). On a completely different note, I'm now looking at writing a compiler for a subset of C, which could eventually become a JIT compiler. If we could attach your GLIL->C compiler to that, it could produce a full Scheme->machine code compiler in Guile. Noah On Wed, Nov 3, 2010 at 7:43 PM, Ludovic Court=C3=A8s wrote: > Hi Stefan, > > Lots of stuff here, which is why I took the time to read it. =C2=A0:-) > > Stefan Israelsson Tampe writes: > >> 1. The theorem prover (leanCop) is a nice exercise > > [...] > >> 2. Kanren is a nice way to program like with prolog, > > Great that you=E2=80=99re mentioning them. =C2=A0It 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. =C2=A0I don=E2=80=99t grok i= t all I=E2=80=99m glad > you=E2=80=99re looking at it from a Guile perspective. =C2=A0:-) > >> 4. The umatch hackity hack was turned into a much more hygienic creature= . > > Funny sentence. =C2=A0:-) > >> 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 g= ood >> idea what is needed. It will be a goos testcase for the code. > > 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-mismatc= h > warnings or determine whether type-checks can be optimized away (which > would require changes in the VM), that=E2=80=99d be great. > > What=E2=80=99s amazing is that Kanren + type-inference.scm weigh in at = =E2=80=9Conly=E2=80=9D > ~3,500 SLOC. > >> 6) I copied the =C2=A0glil->assembly compiler and modded the code to spi= t out >> c-code in stead of assembly. For functions which does not call other sch= eme >> 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 ex= ample >> without consing tok 7ns for each loop on my machine. > > Interesting. =C2=A0Is it a sufficiently isolated change that you could po= int > us to? > > Thanks, > Ludo=E2=80=99. > > >