Re: The progress of hacking guile and prolog

[Stefan Israelsson Tampe]

On Thursday, November 04, 2010 12:43:54 am Ludovic Courtès 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.  :-)

Yes, but I would like to be more true to it then I am right now. So is it 
enough to reproduce minikanren? Also I've reading in on racklog so I guess
what I have right now is correct conceptually but not syntactically. But of
cause this can be fixed. So If you think it is worthwhile I will download the
minikanren sorce hack on.

> > 4. The umatch hackity hack was turned into a much more hygienic creature.
> 
> Funny sentence.  :-)

Well I have two versions one based on the match-phd and is not touching guiles 
internals and is based on passing continuations closures and has the property 
that all calls are tail calls for basic prolog usage patterns. Also note that
this principle is not as expensive that one may think if you take into acount 
a system that inline functions acording to findings from profiling. So in 
principle all this pushing parameters to the heap could be mitigated. The 
other
one is the hackety hack that tend to be fast on the vm.

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

Notes.
        1. It's when compilers start to work you will gain from removing 
        type checks. It's probably not worth it in vm land

        2. If a function is used like (f 0.1) in function g and you recompile
        function f to just allow only fixnums you may end up with havoc. So 
        either function dependencies is tracked or you use the racket way of 
        executing code if going down this optimizing path in a safe way.

        3. Of cause local entities can be tracked and optimized away and maybe
        we should stick to only that.

> What’s amazing is that Kanren + type-inference.scm weigh in at “only”
> ~3,500 SLOC.

Hence is a powerful concept :-)
Hmm I'm also keen to match what typed racket does. I will look into this.


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

Uhmm, I was just curious to se what the overhead of dispatching 
instructions in a goto-loop would give when I did it. But just think of it
as a tool that just inline the c-code behind some simple vm instructions in 
stead of the actual vm-instructions. Actually all prolog vanilla prolog 
code should be able to be compiled quite effectively this way cause it's 
all tail calls. I'm not sure my code is that interesting though Probably the 
idea is more interesting and should be discussed. The basic idea is to pair
the c-code generation with the glil->assembly code so that the compiling
function and all it's internal lambda get's corresponding c-function quite
automagically and then be gcc:d into linkable code and hooked int these 
functions vm part that now just act like a trampoline into C land. 
Do you see it?

Have fun
Stefan