Re: The progress of hacking guile and prolog

[Noah Lavine]

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 (= (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ès <address@hidden> wrote:
> Hi Stefan,
>
> Lots of stuff here, which is why I took the time to read it.  :-)
>
> Stefan Israelsson Tampe <address@hidden> writes:
>
>> 1. The theorem prover (leanCop) is a nice exercise
>
> [...]
>
>> 2. Kanren is a nice way to program like with prolog,
>
> Great that you’re mentioning them.  It looks like there’s a lot of
> interesting work that’s been done around Kanren, such as the “toy” type
> inference engine and, better, αleanTAP.  I don’t grok it all I’m glad
> you’re looking at it from a Guile perspective.  :-)
>
>> 4. The umatch hackity hack was turned into a much more hygienic creature.
>
> Funny sentence.  :-)
>
>> 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 good
>> 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’s compiler, so that it can emit type-mismatch
> warnings or determine whether type-checks can be optimized away (which
> would require changes in the VM), that’d be great.
>
> What’s amazing is that Kanren + type-inference.scm weigh in at “only”
> ~3,500 SLOC.
>
>> 6) I copied the  glil->assembly compiler and modded the code to spit out
>> c-code in stead of assembly. For functions which does not call other scheme
>> 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 example
>> without consing tok 7ns for each loop on my machine.
>
> Interesting.  Is it a sufficiently isolated change that you could point
> us to?
>
> Thanks,
> Ludo’.
>
>
>