What's the state of this library?

[meditans]

Hi, I quite like the fact that your library is one of the few miniKanren-like libraries to have a tentative implementation for lists, instead of the cons-cell lisp hackery.

However, the current state of this library here on github doesn't export Molog.Prelude, and it seems in the middle of a rewrite. What plans do you have for this library? Is there something I can do to help?

[acfoltzer]

I sadly don't have much time to put into it at this point. I'd be interested in work that extends it with a datatypes-à-la-carte approach like Wren's unification-fd package, but don't have any plans for it in the near term.

[meditans]

Hi, could you point me towards papers or resources (I already viewed your talk on Molog on InfoQ) that explain the ideas behind this implementation of Molog?

How are Molog and unification-fd related? What are the respective objectives? Could it be possible to use unification-fd as a base for Molog?

I'm familiar with Data types à la carte, but I'm having trouble to understand the unification-fd package. Are there prerequisite papers that I should be familiar with?

Thanks for the pointers!

[acfoltzer]

The goal of Molog was to embed a miniKanren-style language while being able to still take advantage of Haskell's type system. The biggest stumbling block then is how to bring ordinary Haskell types into the land of logic programming. The LogicList type, for example, is needed to do tree unification with lists, but it would be nice to just use [] instead.

This is an instance of the expression problem, since we essentially want to add a new case (fresh variable) to existing data types. Data types à la carte describes a general technique for avoiding the expression problem by writing your data types as "unfixed" versions of the type you want. The type is now parameterized enough to add additional cases just by applying the appropriate functor to the unfixed type. (The paper does a better job of explaining this than I do)

unification-fd aims to provide heavy duty hardware for this style of unification rather than providing a more specialized embedded DSL. This post is the start of a tutorial for it. Both unification-fd and Molog implement path compression, a common optimization for unification-like algorithms (in fact, expressing path compression in a natural way while in a functional setting was my motivation for creating persistent-refs).

To answer one of your questions, I'd say there's not really enough to Molog beyond the unification operator to make it worth implementing on top of unification-fd. Instead I'd view unification-fd as a heavier-duty version of Molog that takes on the task of unifying arbitrary types in a more principled way than Molog.

[meditans]

Thanks for the explanation, especially the last paragraph which is exactly what I wanted to know. I knew the tutorial you linked, unfortunately I didn't find it particularly enlightening on the library as a whole. I'll try to understand better unification-fd, than. Thanks for the insights!

[acfoltzer]

You're quite welcome!