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: Wed, 24 Nov 2010 17:45:54 +0100 Message-ID: <201011241745.54481.stefan.itampe@gmail.com> References: <201010212223.23822.stefan.itampe@gmail.com> NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: Text/Plain; charset="iso-8859-1" Content-Transfer-Encoding: 7bit X-Trace: dough.gmane.org 1290617124 13981 80.91.229.12 (24 Nov 2010 16:45:24 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Wed, 24 Nov 2010 16:45:24 +0000 (UTC) To: guile-devel@gnu.org Original-X-From: guile-devel-bounces+guile-devel=m.gmane.org@gnu.org Wed Nov 24 17:45:20 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 1PLIT9-0005Fo-N0 for guile-devel@m.gmane.org; Wed, 24 Nov 2010 17:45:20 +0100 Original-Received: from localhost ([127.0.0.1]:55257 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.43) id 1PLIT8-0000w2-W2 for guile-devel@m.gmane.org; Wed, 24 Nov 2010 11:45:18 -0500 Original-Received: from [140.186.70.92] (port=46303 helo=eggs.gnu.org) by lists.gnu.org with esmtp (Exim 4.43) id 1PLIT5-0000vS-LT for guile-devel@gnu.org; Wed, 24 Nov 2010 11:45:16 -0500 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1PLIT4-0001pg-M1 for guile-devel@gnu.org; Wed, 24 Nov 2010 11:45:15 -0500 Original-Received: from mail-ey0-f169.google.com ([209.85.215.169]:41206) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1PLIT4-0001pA-HD for guile-devel@gnu.org; Wed, 24 Nov 2010 11:45:14 -0500 Original-Received: by eydd26 with SMTP id d26so16263942eyd.0 for ; Wed, 24 Nov 2010 08:45:13 -0800 (PST) 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=sw9Dmko9fC0I1kKVNL/OvPyenq/DKdXKef0fvyCwM3I=; b=vainxmcKYed8XP5R11ZX2dzjKaJ8BzKXBC8raM5mi8nl0r2PQ9DIj6jtDwOu8rj2gA xzaBCmDYtBY1kGKVtLS8aB+i8liTMnzyjYzeWh/9fIlEomqFVP9Dqcyj3wN07QRaYVjb eazWmNHOJe8sH6uvHGUtya89xwcuIPvkBC2jE= 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=dS470TUolaF53+lP6ot0SGcaHCSGVAlNfpkIbClQ4R9QE71qsi8Vqv8C/aMM1wI2H2 i52pkWpL6AdZzn53XJHRiYdEr6nPRsH6BkUEqEOGXveA5kiYNZWvzySKcPbJmXbLyPRv hF3PMLjlUt4n7+WjCJXFNsuL3e97A8gnFBh5k= Original-Received: by 10.14.119.1 with SMTP id m1mr7535540eeh.1.1290617113153; Wed, 24 Nov 2010 08:45:13 -0800 (PST) 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 x54sm7118068eeh.23.2010.11.24.08.45.10 (version=TLSv1/SSLv3 cipher=RC4-MD5); Wed, 24 Nov 2010 08:45:11 -0800 (PST) User-Agent: KMail/1.13.5 (Linux/2.6.34.7-0.5-desktop; KDE/4.4.4; x86_64; ; ) In-Reply-To: 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:11194 Archived-At: Hi Noah, On Wednesday, November 24, 2010 02:54:37 am Noah Lavine wrote: > Hello, > > That might make sense. The documentation certainly looks interesting. > > What I'm thinking of is like racket contracts, but with the idea of > "trusted modules", which might involve static checking. For instance, > if the contract is that map's second parameter is a list, you'd > normally want to check that. But if a module that used map could > guarantee that it would always pass a list as the second argument, > then you'd arrange things so the second module could skip the type > check. Sure static typechecking can save some time, but also note that it can bring in applications that would not be on a scheme platform without static typechecking/proofing due to code safety reason imaginable or not (again static versus dynamic). An intersting note, one here stories about codebases around a popular dynamically p.l. where the test harness grow out of bounds and where the major part of it is test that the static typechecker would have been performed by default in both a much faster manner and also more rigourusly. Personally I prefere dynamic - but that is from my usage pattern which is mainly smaller programs that automate. Form this I'm wondering if the people in this hersay really take advantage of testing only the relevant parts of the code in light of done changes. > I'm curious in general though whether it would be possible and > worthwhile to statically check programmer-defined ideas, as long as > the interface is easy enough to use. For instance, what if you could > ask Guile to check that your tree structure always remained a binary > tree? Or better, what if you wrote a GUI program and checked that the > callbacks you passed to the GUI library would always return? (I know > it's not possible in general, but I think it will work for a subset of > procedures that will include some interesting ones.) Yep I agree with you here. Here is an idea: You can try to say something like this function argument will never be returned or kept in a closure etc. Then you might allocate that object from the stack. Again it is not always ways to proove this but sometimes you can. So the function argument could be of a proved not proved and don't know and you can make sure to use the safe way. Then you can guide a user to prove that it is indeed so or let the user say it is so or just take the safe path and allocate from the heap. There is a nice pattern here that one could employ when there is a compiler for guile (without compiler the speedup is not that exiting on a relative scale). Process the code and builed up the result using a tail call paraadigm, e.g. there is a parameter res that is constructed. Then at the end return (heapify (revers ret)) and transfere the constructed ret object to the heap by trying to fill a continuous segment on the heap by cons cells that is linked appropriated. That way you get some work to align objects on the heap, allocate a big chunk at the time and the overall performance scale and is performat. I would say that 99% of the code I write that use or could use this pattern can be typechecked to proove that res could be builed up from stack elements. The typical usage scenario here is to speed up functional (no mutating) code transformations. Have fun Stefan