Re: The progress of hacking guile and prolog

[ludo@gnu.org (Ludovic Courtès)]

Hi!

Noah Lavine <noah.b.lavine@gmail.com> writes:

> 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.

In Guile, modules are dynamic by nature: they are assembled at run-time
(everything is “dynamically linked”).  My feeling is that cross-module
static analysis doesn’t fit well in this framework.

> 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?

I think you’ll be interested in dependent types:

  https://secure.wikimedia.org/wikipedia/en/wiki/Dependent_types

Though I’d recommend working on JIT for Guile before you get stuck in a
meta-circular Curry-Howardish enlightenment period.  :-)

Thanks,
Ludo’.