About internals of faster miniKanren

[Dmitrii Kosarev]

Hey, folks

Can you describe why faster miniKanren [1] is.. em... faster than every think else? I believe that it's true because I measured. Can you put this very useful information in the repo description? What should I do to make microKanren work in the same manner as faster miniKanren.

Happy hacking,
Dmitrii


[1] https://github.com/michaelballantyne/faster-miniKanren

[William Byrd]

Hi Dmitrii!

I'll give a brief answer now. I hope Michael Ballantyne will give a
more detailed explanation. I hope Michael will also go over the
faster-miniKanren implementation during one of the upcoming hangouts.

As I recall, there are three main reasons faster-miniKanren is faster
than previous implementations:

1) use of efficient immutable data structures, rather than association
lists, to implement the substitution, etc. There are other miniKanren
implementations that do this. For a detailed exploration of how
different data structures perform, please see this unpublished paper:

https://www.cs.indiana.edu/~lkuper/papers/walk.pdf

faster-miniKanren doesn't use the absolutely fastest representation,
at least as described in that paper, but any efficient representation
will perform much better than association lists for most real
miniKanren programs.

2) use of attributed variables to represent constraints. That is,
constraints other than unification (disequality, absento, numbero,
symbolo) are associated with logic variables, rather than just being
put in a list as in the original cKanren. The advantage is that it is
quick and easy to determine which constraints are involved in a given
unification. Compare this with the older approach, in which the
entire constraint store might be checked, even when unifying variables
that don't have constraints associated with them.

This is a huge win for programs that make heavy use of constraints,
such as relational interpreters.

As a historical note, I must take the blame for the inefficient
approach used in the original cKanren. Jeremiah Willcock suggested we
use attributed variables from the very beginning, and Claire and Dan
wanted to use them. I wasn't convinced that we'd be able to represent
all of our constraints using attributed variables, and advocated for
the slower, list-based constraint approach. I was wrong.

I believe core.logic uses attributed variables, or something
equivalent, but I'm not sure. Michael Ballantyne wrote a very nice
implementation of our constraints using attributed variables for
faster-mk. I'm not sure if Claire used attributed variables in
Kraken, the successor to cKanren.

Another possibility would be to implement constraints using Constraint
Handling Rules (CHR). I think Claire explored this approach for
Kraken.

3) Michael Ballantyne suggested another optimization, which, to my
knowledge, is only used in faster-miniKanren. Michael noticed that
many times logic variables are unified immediately after they are
created with a 'fresh'. In these cases it is not necessary to extend
the substitution. Instead, we can just mutate a structure
representing the variable (using a local mutation that is harmless).
This is the intent of the 'scope'-related comments in the code:

https://github.com/webyrd/faster-miniKanren/blob/master/mk.scm

Look at the definition of 'subst-add', in particular:

; set-var-val! optimization: set the value directly on the variable
; object if we haven't branched since its creation
; (the scope of the variable and the substitution are the same).
; Otherwise extend the substitution mapping.

I hope Michael will jump in and explain this optimization in more detail.

Hope this helps!

--Will

> --
> You received this message because you are subscribed to the Google Groups
> "minikanren" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to minikanren+...@googlegroups.com.
> To post to this group, send email to minik...@googlegroups.com.
> Visit this group at https://groups.google.com/group/minikanren.
> For more options, visit https://groups.google.com/d/optout.

[Michael Ballantyne]

Oddly enough, I wasn't a member of this list so I didn't see your message until Jason Hemann helpfully forwarded it on to me.

All of what Will writes matches my understanding, and I've written up some more down in the weeds details on the repository README: https://github.com/michaelballantyne/faster-miniKanren#what-makes-it-fast

If you have further questions after reading, I'd be happy to chat during one of the hangouts or via email.

[Nehal Patel]

Thanks Michael -- 

The new faster-mk Readme is very nice!  For a potential further discussion during one of the hangouts, I would be interested in any of the following:

+ I think I have heard Will refer to Barliman's kanren as "d-kanren" (could be wrong?) and apparently this is very fast as well... I'm curious to what extent that version and your faster-mk are similar or different.      

+ Fleshing out the discussion of the constraint implementation a little more.  For instance, various types constraints seem to have the potential to interact with other types of constraints in complicated ways -- making the selection of which types of constraints to support a potentially global design problem (for instance adding finite domains might require reworking all other constraint types or risk poor performance)  Since there have been many different constraint types added to various kanren over the years, I'm curious to understand how people approached this design problem.  

thanks!

To unsubscribe from this group and stop receiving emails from it, send an email to minikanren+unsubscribe@googlegroups.com.

[Dmitrii Kosarev]

Hey, Michael and all

I have some issues about set-var-val optimization  and unification. What happens when you discover part of final prefix which can profit from set-var-val optimization and later whole unification fails? It seems that the one needs to rollback this set-var-val mutation after detecting failure or should postpone set-var-val optimization and apply the prefix in the end of successful unification. I can't detect neither of this approaches in the code of faster-miniKanren. Can you clarify this?

Related code lines
https://github.com/michaelballantyne/faster-miniKanren/blob/master/mk.scm#L91
https://github.com/michaelballantyne/faster-miniKanren/blob/master/mk.scm#L211
https://github.com/michaelballantyne/faster-miniKanren/blob/master/mk.scm#L228

Best regards,
Dmitrii

[Dmitrii Kosarev]

Actually, after some hours it seems that it is impossible to achieve. If it happens just after conde the scope is changed and nothing will go into the variable. And if it happens just after fresh than the fail will not affect anything be cause it will be nothing done in future with variables just created.

[Michael Ballantyne]

Yeah, your analysis in the second email sounds right.

You received this message because you are subscribed to a topic in the Google Groups "minikanren" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/minikanren/NxF15WnfEXk/unsubscribe.
To unsubscribe from this group and all its topics, send an email to minikanren+...@googlegroups.com.

[Dan Friedman]

Dmitrii,

Can you explain exactly what is impossible to achieve and its implications.

... Dan

To unsubscribe from this group and stop receiving emails from it, send an email to minikanren+unsubscribe@googlegroups.com.

[Michael Ballantyne]

I think he meant that the situation he was worried about can't actually cause a bug. This bit:

"you discover part of final prefix which can profit from set-var-val optimization and later whole unification fails"

So, something like:

(fresh (x)

  (== (cons x x) (cons 1 2)))

The set-var-val! optimization performs a side-effect on x that it seems like we might need to roll back when the unification fails, but ultimately it doesn't matter because when the unification fails we throw away all references to x.

You received this message because you are subscribed to a topic in the Google Groups "minikanren" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/minikanren/NxF15WnfEXk/unsubscribe.
To unsubscribe from this group and all its topics, send an email to minikanren+...@googlegroups.com.

[Kakadu]

Michael is correct

To unsubscribe from this group and stop receiving emails from it, send an email to minikanren+unsubscribe@googlegroups.com.

To post to this group, send email to minik...@googlegroups.com.
Visit this group at https://groups.google.com/group/minikanren.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to a topic in the Google Groups "minikanren" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/minikanren/NxF15WnfEXk/unsubscribe.

To unsubscribe from this group and all its topics, send an email to minikanren+unsubscribe@googlegroups.com.

To post to this group, send email to minik...@googlegroups.com.
Visit this group at https://groups.google.com/group/minikanren.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to a topic in the Google Groups "minikanren" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/minikanren/NxF15WnfEXk/unsubscribe.

To unsubscribe from this group and all its topics, send an email to minikanren+unsubscribe@googlegroups.com.

[Dan Friedman]

Thanks.  

... Dan

Sent from my cell phone.

[Amirouche Boubekki]

On Tuesday, March 21, 2017 at 4:59:50 PM UTC+1, William Byrd wrote:

Hi Dmitrii!

I'll give a brief answer now. I hope Michael Ballantyne will give a
more detailed explanation.  I hope Michael will also go over the
faster-miniKanren implementation during one of the upcoming hangouts.

As I recall, there are three main reasons faster-miniKanren is faster
than previous implementations:

1) use of efficient immutable data structures, rather than association
lists, to implement the substitution, etc.  There are other miniKanren
implementations that do this.  For a detailed exploration of how
different data structures perform, please see this unpublished paper:

https://www.cs.indiana.edu/~lkuper/papers/walk.pdf

This paper is gone, can someone upload it somewhere for me please?

Or give a summary of the ideas that are inside?

Also, how do you benchmark (faster-)minikanren?