typedKanren: help me write a `length` predicate

Learn
1

Hey all, I come with a logic programming question, hopefully it is on topic since I am using typedKanren :slightly_smiling_face: .

I tried to write a hasLength :: forall a . Logical a => Term [a] -> Term Binary -> Goal () predicate that relates an arbitrary list to its length. The problem is am not able to make it bidirectional.

I have two implementations, the only difference between them is the order of the last two clauses. Each works in one direction, but none works in both directions:

-- A simple datatype for the example
data Color = R | G | B
  deriving stock (Eq, Show, Generic)

makeLogicals [''Color]
deriving stock instance Show LogicColor

-- The predicate
hasLength :: forall a. Logical a => Term Binary -> Term [a] -> Goal ()
hasLength n ls =
  disj
    do
      zeroo n
      ls & isNil
    do
      (n', t) <- fresh;
      -- Implementation 1:
      ls & hasTail t; t & hasLength n';
      addo n' (inject' 1) n
      -- Implementation 2:
      addo n' (inject' 1) n
      ls & hasTail t; t & hasLength n';

-- One query for each possible direction
queryList :: IO ()
queryList = mapM_ print $ run $ \(ls :: Term [Color]) -> ls & hasLength (inject' 3)

queryLength :: IO ()
queryLength = mapM_ print $ run $ \n -> inject' [R, G, B] & hasLength n

And if I test the queries in ghci, these are the results:

Implementation 1:

ghci> queryList 
[_.4,_.9,_.14]
^CInterrupted.
ghci> queryLength 
[I,I]
ghci>

Implementation 2:

ghci> queryList
[_.23,_.30,_.37]
ghci> queryLength 
[I,I]
^CInterrupted.
ghci>

So, how can I write an implementation that works for both queries? Is it possible?

2 Likes
2

For completeness sake, I provide the definition of hasTail:

hasTail :: forall a. Logical a => Term [a] -> Term [a] -> Goal ()
hasTail t ls = do; h <- fresh; ls & hasHeadTail h t

hasHeadTail :: forall a. Logical a => Term a -> Term [a] -> Term [a] -> Goal ()
hasHeadTail h t l = l & (matche & on _LogicCons (\(h', t') -> h === h' >> t === t'))

The reason I defined these is because I find the pattern matching syntax of typedKanren a little awkward.

3

During the execution of the hasLength predicate, you want the state to keep track of partial knowledge of the values of n and ls. In this case, Binary is not a good representation for the partial knowledge of n. A unary representation is more natural, and one is readily obtained as [()].

{-# LANGUAGE TemplateHaskell, ScopedTypeVariables, DeriveGeneric, DerivingStrategies, BlockArguments, StandaloneDeriving, TypeFamilies, TypeFamilyDependencies #-}

import Kanren.Data.Binary
import Kanren.Core
import Kanren.Match
import Kanren.LogicalBase
import Kanren.Goal
import Kanren.TH
import Data.Maybe
import GHC.Generics
import Data.Function ((&))

-- Needed by Logical [()]
instance Logical () where
  type Logic () = ()
  unify _ _ s = Just s
  walk _ _ = ()
  occursCheck _ _ _ = False
  inject _ = ()
  extract _ = Just ()

-- A simple datatype for the example
data Color = R | G | B
  deriving stock (Eq, Show, Generic)

makeLogicals [''Color]
deriving stock instance Show LogicColor

hasTail :: forall a. Logical a => Term [a] -> Term [a] -> Goal ()
hasTail t ls = do; h <- fresh; ls & hasHeadTail h t

hasHeadTail :: forall a. Logical a => Term a -> Term [a] -> Term [a] -> Goal ()
hasHeadTail h t l = l & (matche & on _LogicCons (\(h', t') -> h === h' >> t === t'))

isNil :: Logical a => Term [a] -> Goal ()
isNil xs = xs & (matche & on _LogicNil (\() -> pure ()))

-- Unary representation
type Unary = [()]

unary :: Int -> Term Unary
unary n = inject' (replicate n ())

ununary :: Unary -> Int
ununary = length

-- The predicate
hasLength :: forall a. Logical a => Term Unary -> Term [a] -> Goal ()
hasLength n ls =
  disj
    do
      n & isNil -- n == 0
      ls & isNil
    do
      (n', t) <- fresh
      n & hasHeadTail (inject' ()) n'  -- n == n' + 1
      ls & hasTail t
      t & hasLength n'

-- One query for each possible direction
queryList :: IO ()
queryList = mapM_ print $ run $ \(ls :: Term [Color]) -> ls & hasLength (unary 3)

queryLength :: IO ()
queryLength = mapM_ (print . ununary . fromJust . extract') $ run $ \n -> inject' [R, G, B] & hasLength n

main :: IO ()
main = do
  queryList
  queryLength
4 Likes
4

This works perfectly, thank you!

I can see that Unary is a more natural representation for this use case (I [de]construct lists one by one, so I only need succ - not addo, poso and friends).

Though I am left wondering what goes wrong exactly when using Binary. Why is information “lost”?

5

On implementation 1:

    do
      (n', t) <- fresh;
      -- Implementation 1:
      ls & hasTail t; t & hasLength n';
      addo n' (inject' 1) n

This unifies the list ls with a cons-cell before recursing with a fresh n'. But if ls is also fresh, then you can keep looping forever. The disj does not help. It adds a base case, but it does not take away the diverging execution that is already there because of the eager recursive call to hasLength made before the unification of n necessary to cut off the search when n is the input.

On implementation 2:

    do
      (n', t) <- fresh;
      -- Implementation 2:
      addo n' (inject' 1) n
      ls & hasTail t; t & hasLength n';

When n and n' are fresh, addo n' (inject' 1) n (where addo is addition on Binary values) basically enumerates pairs of n and n' that satisfy n' + 1 = n. (It’s technically slightly smarter than that, but in no way that substantially improves the situation.) When ls is an input and n is an output, hasLength works by enumerating n (in the addo of the first recursive call), and for each value of n, checking whether n equals the length of ls. Symmetrically to implementation 1 which keeps refining ls forever, implementation 2 will enumerate the right value of n, but also all integers after it. You may get the result you want if you stop the run at the first output, but you will never be sure that it’s the only possible output.

You can see that addo backtracks by just running it with fresh variables. It enumerates possible values of n forever (actually, you can see that each partial value stops at the first zero bit, so it’s smarter than a full enumeration of integers, but that doesn’t avoid the infinite enumeration which is the real issue):

main :: IO ()
main = do
  mapM_ print $ take 10 $ run $ \n -> do
    n' <- fresh
    addo n (inject' 1) n'

{- Output:
[]
[I]
[O,_.19|_.20]
[I,I]
[I,O,_.32|_.33]
[I,I,I]
[I,I,O,_.45|_.46]
[I,I,I,I]
[I,I,I,O,_.58|_.59]
[I,I,I,I,I]
(would go on forever if I didn't take 10)
-}

In contrast, unary addition—implemented with hasHeadTail, which is just unification with a cons cell—does not backtrack. There is a single execution carrying exactly the knowledge that n = n' + 1:

main :: IO ()
main = do
  mapM_ print $ take 10 $ run $ \n -> do
    n' <- fresh
    n & hasHeadTail (inject' ()) n'

{- Output:
[()|_.3]
-}
3 Likes
6

This is a great response, it is much appreciated. I took a few days to study again how recursive logic programming works to finally understand what you said. But now I see why in both implementations termination is not possible.