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: Tue, 23 Nov 2010 20:54:37 -0500 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=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: dough.gmane.org 1290563690 6279 80.91.229.12 (24 Nov 2010 01:54:50 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Wed, 24 Nov 2010 01:54:50 +0000 (UTC) Cc: guile-devel@gnu.org To: Andy Wingo Original-X-From: guile-devel-bounces+guile-devel=m.gmane.org@gnu.org Wed Nov 24 02:54:46 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 1PL4ZK-0007Uu-CL for guile-devel@m.gmane.org; Wed, 24 Nov 2010 02:54:46 +0100 Original-Received: from localhost ([127.0.0.1]:43731 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.43) id 1PL4ZK-0006b2-2x for guile-devel@m.gmane.org; Tue, 23 Nov 2010 20:54:46 -0500 Original-Received: from [140.186.70.92] (port=58002 helo=eggs.gnu.org) by lists.gnu.org with esmtp (Exim 4.43) id 1PL4ZE-0006ax-Pp for guile-devel@gnu.org; Tue, 23 Nov 2010 20:54:41 -0500 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1PL4ZD-0008C8-GX for guile-devel@gnu.org; Tue, 23 Nov 2010 20:54:40 -0500 Original-Received: from mail-wy0-f169.google.com ([74.125.82.169]:59281) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1PL4ZD-0008Bz-BR for guile-devel@gnu.org; Tue, 23 Nov 2010 20:54:39 -0500 Original-Received: by wyf23 with SMTP id 23so11631557wyf.0 for ; Tue, 23 Nov 2010 17:54:38 -0800 (PST) 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=QcH1hoks4dCcuvCPTocet/YVuAR/RqL9jnSI2tCYBE4=; b=UBKyK3R/QJKVZbIyASwzSGX3hmtUKD6Us8NSJ7tCRf7XV0WOjSyCoJS9dOG1OfFuhR 1FBdEAvt7kUZnGZuYVDbaPT9DGTzVfqID+HfHqznYDW+avuxn7qOvFi6D+bH3v3kcrgE t6UMKTdCCBHUvBVzOTYB1fK1biPLjBGu9bpjk= 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=hYhj2+gew4vKubZ+1gHjPqrldlo+Mjdf94HFC2RN4Su6dgEAARBdhDq9jmCwLOIdqW cff5QO2wMsasUhN1axoIkZQgVwr5oSclqCTuVOPQevlmXaR4g6a3UkuY9RawfV0qUgHk rcMTDwziFp3NeyR+tksoBKDBwyUEXa7bmVKXw= Original-Received: by 10.216.180.69 with SMTP id i47mr7489808wem.37.1290563677659; Tue, 23 Nov 2010 17:54:37 -0800 (PST) Original-Received: by 10.216.237.34 with HTTP; Tue, 23 Nov 2010 17:54:37 -0800 (PST) In-Reply-To: X-Google-Sender-Auth: WoXPa8HzrXELN7BEMyToGH00IF4 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:11193 Archived-At: 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. 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.) Noah On Sat, Nov 20, 2010 at 6:25 AM, Andy Wingo wrote: > Hi Noah, > > On Thu 04 Nov 2010 03:40, Noah Lavine writes: > >> I think that Guile should offer optional static checking - not just of >> types, but of everything that we can check. > > It seems like you're really asking for *dynamic* checking -- not only > checking properties that can be proved statically, without running the > program, but also runtime properties. > > In this regard, I have a positive impression of the work that people are > doing on "contracts", especially the Racket folks. > > =A0 =A0http://docs.racket-lang.org/reference/contracts.html > > Happy reading, > > Andy > -- > http://wingolog.org/ >