[ANN] shen-minikanren

[Mark Thom]

I've posted an embedding of miniKanren into Shen:

https://github.com/mthom/shen-minikanren

It could use a lot of work, to reduce the number of type inferences, pack it up into a module, 

tighten up the type theory, etc. The github README contains some information on how to integrate queries 

into the type system. 

In the next while I'm going to try implementing the Shen type checker (written mostly in Prolog, I think)

in miniKanren.

[fuzzy wozzy]

what exactly is minikanren?
is it to introduce logic programming to an existing language?
if so, why does it also apply to languages like prolog when prolog is already a  logic-based language?
is it a higher order logic as opposed to a first order logic?
what new features or paradigms does it bring to procedural/object-oriented/functional/logic-based/array-based languages?
what can it make shen do that shen doesn't do already?
very confusing...

[Mark Thom]

miniKanren is an embedded DSL for logic programming. Yes, it adds logic programming to an existing language.

I agree, it seems like a redundant addition to Shen, since we already have built-in Prolog and backtracking. I think the main selling point 

is that it can easily be made to support typed logic programming, similar to what you'd have in a language like Mercury, 

which cannot be said for Prolog. 

As well, the project might pique the interest of the miniKanren folks, who are rooted in the Scheme community and who, like us,

are interested in blending functional and logic programming.

[jpd]

A few questions:

(a) Why are unit lambdaf@ and lambdag@ necessary? They are either not used (unit) or straight up renamings of
better understood names (lambdaf@ => freeze, lambdag@ => /.) and increase cognitive load while trying to
read the code. Is it to conform to the vocabulary to the original paper?

(b) mzero, I am familiar with from Haskell, however it is not used at all, so I'm not sure why it exists. I see that you
define an mplus function, maybe you should be using mzero there? I wonder if there might be better names for
mplus or mzero. Haskell has to have generic names for these since they interface a typeclass, but Shen doesn't have
typeclasses so I suspect these have a specific meaning for a specific type, but I haven't looked to closely into
it so I don't know for sure.

[Mark Thom]

Yes, the additional names are there to maintain the vocabulary of the paper / book, and also as a marker
to indicate what came from where. mplus and mzero, as in Haskell, refer to the traits of a monoid, ie.
monoidal addition and identity, so that sense they're appropriate here also. I agree that mzero should
probably be removed, or I should begin using it appropriately.

[fuzzy wozzy]

someone wrote on amazon review explaining how intent becomes clear and obvious
when expressed in haskell rather than in scheme macros, all in one screen,
don't know haskell but the whole thing looked simple, can't imagine shen would be
longer or more complicated than the haskell version shown on the review.
simple isn't always the best, but sometimes it can be.

[fuzzy wozzy]

is there a simple example on how to use the shen minikanren?

[Mark Thom]

The file tests.shen contains lots of simple examples. Nothing in the way of expository text, I'm afraid. I may write something along those lines in the near future.

[Mark Thom]

Yes, I read that Amazon review. Oleg Kiselyov, one of The Reasoned Schemer authors, did some related work on enabling a similar style of logic programming in Haskell (the LogicT monad),
and it was a lot more complex than what the reviewer anticipated. There's a fairly dense paper Kiselyov et al wrote on their efforts.

Also, it's not helped by the use of algebraic data types, which are required in Haskell and add a lot of verbosity to the code. Like Scheme, Shen doesn't have to deal with them.

[Mark Thom]

Oh, and here's a miniKanren tutorial that uses Clojure syntax: http://objectcommando.com/blog/2011/11/04/the-magical-island-of-kanren-core-logic-intro-part-1/

It should be straightforward to translate it into Shen, if you go by the examples. Later in the week I'll post a table to the project README detailing the (very minor) differences between
shen-minikanren syntax and that of Scheme.