From: ludo@gnu.org (Ludovic Courtès)
To: guile-devel@gnu.org
Subject: Re: A Plan for Hacking
Date: Sun, 25 Sep 2011 22:50:38 +0200 [thread overview]
Message-ID: <8762kg4a8x.fsf@gnu.org> (raw)
In-Reply-To: CA+U71=PxsvkuUaZbLigW+vxwyCF5vgJhYPJuVn0S6+_8kXdqnA@mail.gmail.com
Hi Noah!
Noah Lavine <noah.b.lavine@gmail.com> skribis:
> I think the next step is to write a static analyzer. This analyzer
> will be used by the compiler, but it will not just be for the compiler
> - it will also be available to users. I think of it as a tool for
> writing correct programs. Here are some use-cases for a static
> analyzer:
> - You write a function that assumes its arguments are of a certain
> type. You'd like to be sure this is true, so your program won't throw
> exceptions in the middle.
That would be cool. However, I suspect that for best results you’d want
procedures to have type annotations, as in Racket’s Typed Scheme and
Bigloo; otherwise it may be impossible to determine type info most of
the time—e.g., a public top-level procedure used in another module.
(It’s not clear to me whether this can be done without seriously
compromising on dynamic module composition.)
> - You write a program with more than one thread, which includes a
> series of mutexes. You'd like to verify that if a thread grabs more
> than one of these mutexes, then it always does so in a certain order.
> - You write a program that will respond to HTTP requests. You'd like
> to verify that information from a certain set of variables only
> influences your response packets if the user has a certain cookie
> (i.e. verify that your web server is secure).
> - You write some C code that manipulates Guile values. You'd like to
> be sure that the code does all of the appropriate Guile typechecks
> before using Guile library functions. (This is taken from the Guile
> to-do list, on the website.)
These three items seem “off-topic” and less important to me.
> - You write a compiler for Guile code. You'd like to infer the types
> of variables at compile-time.
Cool!
[...]
> So this is my proposal for the next several months: I work on a static
> analyzer for Guile, hoping to expand it to other languages as well.
> The main goal will be to make it very easy to use this analyzer in
> code, including providing helpful feedback to users when their
> assertions fail. While developing this, I will make sure that it can
> check things that would be useful to a compiler. Once we have a static
> analyzer, we can use it as the first step in an optimizing compiler.
>
> What do you think?
Sounds like a nice plan. :-)
To reduce frustration, I would narrow the use cases a bit, or define
short-term milestones. For instance, you could decide to focus solely
on type inference, or have type inference one of your major milestones.
Kanren [0] and its companion book look like nice starting points to me.
In particular, there’s a simple type inference engine written in Kanren
that is actually usable with Guile 2.0 out of the box and could serve as
a starting point.
And before that, make sure PEG actually gets merged. ;-)
Thanks,
Ludo’.
[0] http://kanren.sourceforge.net/
next prev parent reply other threads:[~2011-09-25 20:50 UTC|newest]
Thread overview: 9+ messages / expand[flat|nested] mbox.gz Atom feed top
2011-09-24 23:58 A Plan for Hacking Noah Lavine
2011-09-25 20:50 ` Ludovic Courtès [this message]
2011-09-25 22:33 ` Noah Lavine
2011-09-26 9:11 ` Marijn
2011-09-26 11:10 ` William ML Leslie
2011-09-26 10:31 ` Stefan Israelsson Tampe
2011-09-28 9:38 ` Ludovic Courtès
2011-09-28 18:05 ` Noah Lavine
2012-01-04 18:29 ` Andy Wingo
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
List information: https://www.gnu.org/software/guile/
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=8762kg4a8x.fsf@gnu.org \
--to=ludo@gnu.org \
--cc=guile-devel@gnu.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).