Initial commit

LICENSE

@@ -0,0 +1,30 @@
+Copyright Filippo Sestini (c) 2018
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Author name here nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

README.md

@@ -0,0 +1,54 @@
+# mu-kanren
+
+Haskell implementation of
+[μKanren](http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf), a
+minimalist language in the miniKanren family of relational (logic) programming
+languages.
+
+It is not meant to be an actual runnable program, but rather a core library to
+experiment with on the repl.
+
+# Build & use
+
+```
+$ cabal new-repl
+```
+
+# Examples
+
+Some examples taken from the
+[repository](https://github.com/jasonhemann/microKanren) of the original Scheme
+implementation.
+
+```
+λ> takeS 2 aAndB
+([(#1, 5), (#0, 7)], 2)
+([(#1, 6), (#0, 7)], 2)
+
+λ> takeS 1 (fives (num 5))
+([], 0)
+
+-- limit number of recursive calls
+-- to avoid divergence.
+λ> takeS' 1 10 (fives (num 3))
+λ>
+
+λ> takeS 2 callAppendo
+([(#0, (#1 #2 #3)), (#2, #3), (#1, ())], 4)
+([(#0, (#1 #2 #3)), (#2, #6), (#5, ()), (#3, (#4 . #6)), (#1, (#4 . #5))], 7)
+
+λ> run 2 callAppendo
+(() _.0 _.0)
+((_.0) _.1 (_.0 . _.1))
+
+λ> runAll appendoo
+(() (1 2 3 4 5))
+((1) (2 3 4 5))
+((1 2) (3 4 5))
+((1 2 3) (4 5))
+((1 2 3 4) (5))
+((1 2 3 4 5) ())
+
+
+
+```

Setup.hs

@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain

app/Main.hs

@@ -0,0 +1,10 @@
+module Main where
+
+import DStream
+import MuKanren
+import Programs
+import Term
+import Wrappers
+
+main :: IO ()
+main = putStrLn "Welcome to Micro Kanren!"

mu-kanren.cabal

@@ -0,0 +1,58 @@
+-- This file has been generated from package.yaml by hpack version 0.21.2.
+--
+-- see: https://github.com/sol/hpack
+--
+-- hash: ac17752394bf78de8ec919e5211d3eda98919dcfbb31bc4b8a52f740f25529f0
+
+name:           mu-kanren
+version:        0.1.0.0
+description:    Please see the README on Github at <https://github.com/fsestini/mu-kanren#readme>
+homepage:       https://github.com/fsestini/mu-kanren#readme
+bug-reports:    https://github.com/fsestini/mu-kanren/issues
+author:         Filippo Sestini
+maintainer:     [email protected]
+copyright:      2018 Filippo Sestini
+license:        BSD3
+license-file:   LICENSE
+build-type:     Simple
+cabal-version:  >= 1.10
+
+extra-source-files:
+    README.md
+
+source-repository head
+  type: git
+  location: https://github.com/fsestini/mu-kanren
+
+library
+  exposed-modules:
+      DStream
+      MuKanren
+      Programs
+      Term
+      Wrappers
+  other-modules:
+      Paths_mu_kanren
+  hs-source-dirs:
+      src
+  build-depends:
+      base >=4.7 && <5
+    , mtl
+    , s-cargot
+    , text
+  default-language: Haskell2010
+
+executable mu-kanren-exe
+  main-is: Main.hs
+  other-modules:
+      Paths_mu_kanren
+  hs-source-dirs:
+      app
+  ghc-options: -threaded -rtsopts -with-rtsopts=-N
+  build-depends:
+      base >=4.7 && <5
+    , mtl
+    , mu-kanren
+    , s-cargot
+    , text
+  default-language: Haskell2010

package.yaml

@@ -0,0 +1,32 @@
+name:                mu-kanren
+version:             0.1.0.0
+github:              "fsestini/mu-kanren"
+license:             BSD3
+author:              "Filippo Sestini"
+maintainer:          "[email protected]"
+copyright:           "2018 Filippo Sestini"
+
+extra-source-files:
+- README.md
+
+description:         Please see the README on Github at <https://github.com/fsestini/mu-kanren#readme>
+
+dependencies:
+- base >= 4.7 && < 5
+- s-cargot
+- mtl
+- text
+
+library:
+  source-dirs: src
+
+executables:
+  mu-kanren-exe:
+    main:                Main.hs
+    source-dirs:         app
+    ghc-options:
+    - -threaded
+    - -rtsopts
+    - -with-rtsopts=-N
+    dependencies:
+    - mu-kanren

src/DStream.hs

@@ -0,0 +1,36 @@
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE DeriveFoldable #-}
+{-# LANGUAGE DeriveTraversable #-}
+
+module DStream where
+
+import Control.Monad
+
+data DStream a = Nil | Cons a (DStream a) | Delay (DStream a)
+  deriving (Show, Functor, Foldable, Traversable)
+
+foldS :: (a -> b -> b) -> (b -> b) -> b -> DStream a -> b
+foldS f g z Nil = z
+foldS f g z (Cons x xs) = f x (foldS f g z xs)
+foldS f g z (Delay xs) = g (foldS f g z xs)
+
+instance Applicative DStream where
+  pure = flip Cons Nil
+  (<*>) = ap
+
+instance Monad DStream where
+  return = flip Cons Nil
+  xs >>= f = join' $ fmap f xs
+    where cat ys = foldS Cons Delay ys ; join' = foldS (flip cat) Delay Nil
+
+interleave :: DStream a -> DStream a -> DStream a
+interleave Nil ys = ys
+interleave (Delay xs) ys = Delay $ interleave ys xs
+interleave (Cons x xs) ys = Cons x (interleave ys xs)
+
+takeLimit :: Int -> Int -> DStream a -> DStream a
+takeLimit 0 _ _ = Nil
+takeLimit n l Nil = Nil
+takeLimit n l (Cons x xs) = Cons x (takeLimit (n - 1) l xs)
+takeLimit n 0 (Delay xs) = Nil
+takeLimit n l (Delay xs) = Delay (takeLimit n (l - 1) xs)

src/MuKanren.hs

@@ -0,0 +1,39 @@
+module MuKanren where
+
+import Term
+import DStream
+
+import Data.Bool
+
+type Sub = [(Var, Term)]
+type State = (Sub, Int)
+type Res = DStream State
+type Goal = State -> Res
+
+walk :: Term -> Sub -> Term
+walk t@(TVar v) s = maybe t (flip walk s) (lookup v s)
+walk t s = t
+
+unify :: Term -> Term -> Sub -> Maybe Sub
+unify u v s = aux (walk u s) (walk v s)
+  where
+    aux :: Term -> Term -> Maybe Sub
+    aux (TVar u) (TVar v) | u == v = Just s
+    aux (TVar u) v = Just ((u, v) : s)
+    aux u (TVar v) = Just ((v, u) : s)
+    aux (TPair u v) (TPair u' v') = aux u u' >>= unify v v'
+    aux (TData x) (TData y) = x ~= y >>= bool Nothing (Just s)
+    aux _ _ = Nothing
+
+(===) :: Term -> Term -> Goal
+(u === v) st = maybe Nil (\nu -> pure (nu, snd st)) (unify u v (fst st))
+
+callFresh :: (Var -> Goal) -> Goal
+callFresh f sc = f c (fst sc , c + 1) where c = snd sc
+
+conj, disj :: Goal -> Goal -> Goal
+disj g1 g2 sc = interleave (g1 sc) (g2 sc)
+conj g1 g2 sc = g1 sc >>= g2
+
+emptyState :: State
+emptyState = ([], 0)

src/Programs.hs

@@ -0,0 +1,44 @@
+module Programs where
+
+import MuKanren
+import Wrappers
+import Term
+import DStream
+
+aAndB :: Goal
+aAndB = conj (callFresh (\a -> TVar a === num 7))
+             (callFresh (\b -> disj (TVar b === num 5) (TVar b === num 6)))
+
+fives :: Term -> Goal
+fives x = disj (x === num 5) (Delay . fives x)
+
+appendo :: Term -> Term -> Term -> Goal
+appendo l s o =
+  disj (conj (nil === l) (s === o)) $ runG $ do
+    [a,d,r] <- fresh 3
+    pure $ conjs [ TPair (TVar a) (TVar d) === l
+                 , TPair (TVar a) (TVar r) === o
+                 , appendo (TVar d) s (TVar r) ]
+
+callAppendo :: Goal
+callAppendo = runG $ do
+  [q,l,s,out] <- fresh 4
+  pure $ conj (appendo (TVar l) (TVar s) (TVar out))
+              (list [TVar l, TVar s, TVar out] === TVar q)
+
+appendoo :: Goal
+appendoo = runG $ do
+  [q,x,y] <- fresh 3
+  pure $ conj (appendo (TVar x) (TVar y) (nums [1,2,3,4,5]))
+              (list [TVar x, TVar y] === TVar q)
+
+relo :: Term -> Goal
+relo x = runG $ do
+  [x1,x2] <- fresh 2
+  pure $ conj (x === TPair (TVar x1) (TVar x2))
+              (disj (TVar x1 === TVar x2)
+                    (Delay . relo x))
+
+manyNonAns :: Goal
+manyNonAns = callFresh $ \x ->
+  disj (relo (TPair (num 5) (num 6))) (TVar x === num 3)

src/Term.hs

@@ -0,0 +1,50 @@
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE GADTs #-}
+
+module Term where
+
+import Type.Reflection
+import Data.SCargot
+import Data.SCargot.Repr.Basic
+import Data.Text (Text, pack, unpack)
+
+type Var = Int
+
+data Atom where
+  AVar :: Var -> Atom
+  AData :: (Eq a, Show a, Typeable a) => a -> Atom
+
+instance Show Atom where
+  show (AVar v) = "AVar " ++ show v
+  show (AData d) = "AData " ++ show d
+
+(~=) :: (Eq a, Typeable a, Typeable b) => a -> b -> Maybe Bool
+x ~= y = fmap (\HRefl -> x == y) (eqTypeRep (typeOf x) (typeOf y))
+
+type Term = SExpr Atom
+
+pattern TPair a t = a ::: t
+pattern TVar v = A (AVar v)
+pattern TData d = A (AData d)
+
+nil :: Term
+nil = Nil
+
+printAtom :: Atom -> Text
+printAtom (AVar v) = pack ("#" ++ show v)
+printAtom (AData d) = pack (show d)
+
+printer :: SExprPrinter Atom Term
+printer = setIndentStrategy (const Align) $ basicPrint printAtom
+
+printTerm :: Term -> String
+printTerm = unpack . encodeOne printer
+
+num :: Int -> Term
+num = TData
+
+nums :: [Int] -> Term
+nums = list . fmap num
+
+list :: [Term] -> Term
+list = foldr TPair nil