diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,20 @@ +Copyright (c) 2014 Danny Gratzer + +Permission is hereby granted, free of charge, to any person obtaining +a copy of this software and associated documentation files (the +"Software"), to deal in the Software without restriction, including +without limitation the rights to use, copy, modify, merge, publish, +distribute, sublicense, and/or sell copies of the Software, and to +permit persons to whom the Software is furnished to do so, subject to +the following conditions: + +The above copyright notice and this permission notice shall be included +in all copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. +IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY +CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, +TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE +SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/ds-kanren.cabal b/ds-kanren.cabal new file mode 100644 --- /dev/null +++ b/ds-kanren.cabal @@ -0,0 +1,101 @@ +name: ds-kanren +version: 0.2.0.0 +synopsis: A subset of the miniKanren language +description: + ds-kanren is an implementation of the language. + . + == What's in ds-kanren? + . + ['disconj'] + Try the left and the right and gather solutions that satisfy + either one. + ['fresh'] + Create a fresh logical variable + ['==='] + Equate two terms. This will backtrack if we can't unify + them in this branch. + ['run'] + Actually run a logical computation and return results and + the constraints on them. + . + In addition to these core combinators, we also export a few + supplimentary tools. + . + ['=/='] + The opposite of '===', ensure that the left and right + never unify. + . + == The Classic Example + . + We can define the classic @appendo@ relationship by encoding + lists in the Lisp "bunch-o-pairs" method. + . + > appendo :: Term -> Term -> Term -> Predicate + > appendo l r o = + > conde [ program [l === "nil", o === r] + > , manyFresh $ \h t o -> + > program [ Pair h t === l + > , appendo t r o + > , Pair h o === o ]] + . + Once we have a relationship, we can run it backwards and forwards + as we can with most logic programs. + . + >>> let l = list ["foo", "bar"] + . + >>> map fst . runN 1 $ \t -> appendo t l l + [nil] + >>> map fst . runN 1 $ \t -> appendo l t l + [nil] + >>> map fst . runN 1 $ \t -> appendo l l t + [(foo, (bar, (foo, (bar, nil))))] + . + == Related Links + . + Some good places to start learning about miniKanren would be + . + * + * + * +license: MIT +license-file: LICENSE +author: Danny Gratzer +maintainer: jozefg@cmu.edu +category: Language +build-type: Simple +cabal-version: >=1.10 +source-repository head + type: hg + location: http://bitbucket.org/jozefg/ds-kanren + +library + exposed-modules: Language.DSKanren + , Language.DSKanren.Core + , Language.DSKanren.Sugar + build-depends: base >=4 && <5 + , containers >=0.4 + , logict + hs-source-dirs: src + default-language: Haskell2010 +Test-Suite test-unify: + hs-source-dirs: test + type: exitcode-stdio-1.0 + main-is: Unify.hs + hs-source-dirs: test + build-depends: ds-kanren + , tasty + , tasty-quickcheck + , QuickCheck + , base >=4 && <5 + default-language: Haskell2010 +Test-Suite test-list-ops: + hs-source-dirs: test + type: exitcode-stdio-1.0 + main-is: List.hs + hs-source-dirs: test + build-depends: ds-kanren + , tasty + , tasty-quickcheck + , QuickCheck + , base >=4 && <5 + default-language: Haskell2010 diff --git a/src/Language/DSKanren.hs b/src/Language/DSKanren.hs new file mode 100644 --- /dev/null +++ b/src/Language/DSKanren.hs @@ -0,0 +1,7 @@ +-- | The toplevel module exports the core language, in +-- 'Language.DSKanren.Core' and some simple combinators from +-- 'Language.DSKanren.Sugar'. +module Language.DSKanren ( module Language.DSKanren.Core + , module Language.DSKanren.Sugar ) where +import Language.DSKanren.Core +import Language.DSKanren.Sugar diff --git a/src/Language/DSKanren/Core.hs b/src/Language/DSKanren/Core.hs new file mode 100644 --- /dev/null +++ b/src/Language/DSKanren/Core.hs @@ -0,0 +1,157 @@ +{-# LANGUAGE RecordWildCards #-} +module Language.DSKanren.Core ( Term(..) + , Var + , Neq + , (===) + , (=/=) + , fresh + , conj + , disconj + , Predicate + , failure + , success + , currentGoal + , run ) where +import Control.Monad.Logic +import Data.String +import qualified Data.Map as M + +-- | The abstract type of variables. As a consumer you should never +-- feel the urge to manipulate these directly. +newtype Var = V Integer deriving (Eq, Ord) + +instance Show Var where + show (V i) = '_' : show i + +suc :: Var -> Var +suc (V i) = V (i + 1) + +-- | The terms of our logical language. +data Term = Var Var -- ^ Logical variables that can unify with other terms + | Atom String -- ^ The equivalent of Scheme's symbols or keywords + | Pair Term Term -- ^ Pairs of terms + deriving Eq + +instance Show Term where + show t = case t of + Var v -> show v + Atom a -> '\'' : a + Pair l r -> "(" ++ show l ++ ", " ++ show r ++ ")" + +instance IsString Term where + fromString = Atom + +type Sol = M.Map Var Term + +-- | Substitute all bound variables in a term giving the canonical +-- term in an environment. Sometimes the solution isn't canonical, +-- so some ugly recursion happens. Happily we don't have to prove +-- normalization. +canonize :: Sol -> Term -> Term +canonize sol t = case t of + Atom a -> Atom a + Pair l r -> canonize sol l `Pair` canonize sol r + Var i -> maybe (Var i) (canonize $ M.delete i sol) $ M.lookup i sol + +-- | Ensures that a variable doesn't occur in some other term. This +-- prevents us from getting some crazy infinite term. None of that +-- nonsense. +notIn :: Var -> Term -> Bool +notIn v t = case t of + Var v' -> v /= v' + Atom _ -> True + Pair l r -> notIn v l && notIn v r + +-- | Extend an environment with a given term. Note that +-- that we don't even bother to canonize things here, that +-- can wait until we extact a solution. +extend :: Var -> Term -> Sol -> Sol +extend = M.insert + +-- | Unification cannot need not backtrack so this will either +-- universally succeed or failure. Tricksy bit, we don't want to allow +-- infinite terms since that can be narly. To preserve reflexivity, we +-- have a special check for when we compare a var to itself. This +-- doesn't extend the enviroment. With this special case we can add a +-- check to make sure we never unify a var with a term containing it. +unify :: Term -> Term -> Sol -> Maybe Sol +unify l r sol= case (l, r) of + (Atom a, Atom a') | a == a' -> Just sol + (Pair h t, Pair h' t') -> unify h h' sol >>= unify t t' + (Var i, Var j) | i == j -> Just sol + (Var i, t) | i `notIn` t -> Just (extend i t sol) + (t, Var i) | i `notIn` t -> Just (extend i t sol) + _ -> Nothing + +type Neq = (Term, Term) +data State = State { sol :: Sol + , var :: Var + , neq :: [Neq] } +newtype Predicate = Predicate {unPred :: State -> Logic State} + +-- | Validate the inqualities still hold. +-- To do this we try to unify each pair under the current +-- solution, if this fails we're okay. If they *don't* then +-- make sure that the solution under which they unify is an +-- extension of the solution set, ie we must add more facts +-- to get a contradiction. +checkNeqs :: State -> Logic State +checkNeqs s@State{..} = foldr go (return s) neq + where go (l, r) m = + case unify (canonize sol l) (canonize sol r) sol of + Nothing -> m + Just badSol -> if domain badSol == domain sol then mzero else m + domain = M.keys + +-- | Equating two terms will attempt to unify them and backtrack if +-- this is impossible. +(===) :: Term -> Term -> Predicate +(===) l r = Predicate $ \s@State {..} -> + case unify (canonize sol l) (canonize sol r) sol of + Just sol' -> checkNeqs s{sol = sol'} + Nothing -> mzero + +-- | The opposite of unification. If any future unification would +-- cause these two terms to become equal we'll backtrack. +(=/=) :: Term -> Term -> Predicate +(=/=) l r = Predicate $ \s@State{..} -> checkNeqs s{neq = (l, r) : neq} + +-- | Generate a fresh (not rigid) term to use for our program. +fresh :: (Term -> Predicate) -> Predicate +fresh withTerm = + Predicate $ \State{..} -> + unPred (withTerm $ Var var) $ State sol (suc var) neq + +-- | Conjunction. This will return solutions that satsify both the +-- first and second predicate. +conj :: Predicate -> Predicate -> Predicate +conj p1 p2 = Predicate $ \s -> unPred p1 s >>- unPred p2 + +-- | Disjunction. This will return solutions that satisfy either the +-- first predicate or the second. +disconj :: Predicate -> Predicate -> Predicate +disconj p1 p2 = Predicate $ \s -> unPred p1 s `interleave` unPred p2 s + +-- | The Eeyore of predicates, always fails. This is mostly useful as +-- a way of pruning out various conditions, as in +-- @'conj' (a '===' b) 'failure'@. This is also an identity for +-- 'disconj'. +failure :: Predicate +failure = Predicate $ const mzero + +-- | The Tigger of predicates! always passes. This isn't very useful +-- on it's own, but is helpful when building up new combinators. This +-- is also an identity for 'conj'. +success :: Predicate +success = Predicate return + +-- | The goal that this logic program is trying to create. This is +-- occasionally useful when we're doing generating programs. +currentGoal :: Term +currentGoal = Var (V 0) + +-- | Run a program and find all solutions for the parametrized term. +run :: (Term -> Predicate) -> [(Term, [Neq])] +run mkProg = map answer . observeAll $ prog + where prog = unPred (fresh mkProg) (State M.empty (V 0) []) + answer State{..} = (canonize sol . Var $ V 0, neq) diff --git a/src/Language/DSKanren/Sugar.hs b/src/Language/DSKanren/Sugar.hs new file mode 100644 --- /dev/null +++ b/src/Language/DSKanren/Sugar.hs @@ -0,0 +1,35 @@ +{-# LANGUAGE FlexibleInstances #-} +module Language.DSKanren.Sugar where +import Language.DSKanren.Core + +-- | Disjunction of many clauses. This can be thought as a logical +-- switch. +conde :: [Predicate] -> Predicate +conde = foldr disconj failure + +-- | Conjuction of many clauses. Think of this as a sort of logical +-- semicolon. +program :: [Predicate] -> Predicate +program = foldr conj success + +-- | Only grab n solutions. Useful for when the full logic program +-- might not terminate. Or takes its sweet time to do so. +runN :: Int -> (Term -> Predicate) -> [(Term, [Neq])] +runN n = take n . run + +-- | We often want to introduce many fresh variables at once. We've +-- encoded this in DSKanren with the usual type class hackery for +-- variadic functions. +class MkFresh a where + -- | Instantiate @a@ with as many fresh terms as needed to produce a + -- predicate. + manyFresh :: a -> Predicate +instance MkFresh a => MkFresh (Term -> a) where + manyFresh = fresh . fmap manyFresh +instance MkFresh Predicate where + manyFresh = id + +-- | Build a lispish list out of terms. The atom @"nil"@ will serve as +-- the empty list and 'Pair' will be ':'. +list :: [Term] -> Term +list = foldr Pair (Atom "nil") diff --git a/test/List.hs b/test/List.hs new file mode 100644 --- /dev/null +++ b/test/List.hs @@ -0,0 +1,47 @@ +{-# LANGUAGE OverloadedStrings #-} +module Main where +import Language.DSKanren +import Test.Tasty.QuickCheck hiding ((===)) +import Test.Tasty +import QuickCheckHelper + +appendo :: Term -> Term -> Term -> Predicate +appendo l r o = + conde [ program [l === "nil", o === r] + , manyFresh $ \h t o' -> + program [ Pair h t === l + , appendo t r o' + , Pair h o' === o ]] + +heado :: Term -> Term -> Predicate +heado l h = fresh $ \t -> Pair h t === l + +tailo :: Term -> Term -> Predicate +tailo l t = fresh $ \h -> Pair h t === l + +isAppend :: TestTree +isAppend = testProperty "Head Works" + . mapSize (const 3) + . forAll (two . listOf1 $ mkTerm []) + $ \(l, r) -> case runN 1 $ appendo (list l) (list r) of + (t, _) : _ -> t == list (l ++ r) + _ -> False + +isHead :: TestTree +isHead = testProperty "Head Works" + . mapSize (const 3) + . forAll (listOf1 $ mkTerm []) + $ \terms -> case runN 1 $ heado (list terms) of + (t, _) : _ -> t == head terms + _ -> False + +isTail :: TestTree +isTail = testProperty "Tail Works" + . mapSize (const 3) + . forAll (listOf1 $ mkTerm []) + $ \terms -> case runN 1 $ tailo (list terms) of + (t, _) : _ -> t == list (tail terms) + _ -> False + +main :: IO () +main = defaultMain (testGroup "List Tests" [isHead, isTail]) diff --git a/test/Unify.hs b/test/Unify.hs new file mode 100644 --- /dev/null +++ b/test/Unify.hs @@ -0,0 +1,134 @@ +-- | Test to ensure that unification function as intended. +module Main where +import Language.DSKanren +import Test.Tasty +import Test.Tasty.QuickCheck hiding ((===)) +import QuickCheckHelper + +--------------------------- Equal ------------------------------------- +eqrefl :: TestTree +eqrefl = testProperty "Reflexivity" + . forTerm + $ \t -> hasSolution (t === t) + +eqcomm :: TestTree +eqcomm = testProperty "Commutative" + . forTerm2 + $ \ l r -> + hasSolution (l === r) + ==> hasSolution (r === l) + +eqtrans :: TestTree +eqtrans = testProperty "Transitive" + . forTerm3 + $ \l m r -> + hasSolution (conj (l === m) (m === r)) + ==> hasSolution (r === l) + +eqTests :: TestTree +eqTests = testGroup "Equality" [eqrefl, eqcomm, eqtrans] + +------------------------ Not Equal ----------------------------------- +neqarefl :: TestTree +neqarefl = testProperty "Antireflexive" + . forTerm + $ \t -> not $ hasSolution (t =/= t) + +neqcomm :: TestTree +neqcomm = testProperty "Commutative" + . forTerm2 + $ \ l r -> + hasSolution (l =/= r) + ==> hasSolution (r =/= l) + +neqTests :: TestTree +neqTests = testGroup "Inequality" [neqarefl, neqcomm] + + +--------------------------- Fresh ------------------------------------ +freshClosed :: TestTree +freshClosed = testProperty "Closed Under Fresh" + . forPred + $ \p -> hasSolution p ==> hasSolution (fresh $ const p) +freshUnify :: TestTree +freshUnify = testProperty "Unification Under Fresh" + . forTerm + $ \t -> forPred $ \p -> + hasSolution p + ==> hasSolution . fresh $ \v -> conj (t === v) p + +freshTests :: TestTree +freshTests = testGroup "Fresh" [freshClosed, freshUnify] + +--------------------------- Conj ------------------------------------- +conjid :: TestTree +conjid = testProperty "Commutative" + . forPred + $ \p -> hasSolution p ==> hasSolution (conj success p) + +conjcomm :: TestTree +conjcomm = testProperty "Commutative" + . forPred2 + $ \p o -> + hasSolution (conj p o) ==> hasSolution (conj o p) + +conjassoc :: TestTree +conjassoc = testProperty "Associative" + . forPred3 + $ \l m r -> + hasSolution (conj (conj l m) r) + ==> hasSolution (conj l (conj m r)) + +conjTests :: TestTree +conjTests = testGroup "Conj" [conjid, conjcomm, conjassoc] + +------------------------- Disconj ------------------------------------ +disconjid :: TestTree +disconjid = testProperty "Commutative" + . forPred + $ \p -> hasSolution p ==> hasSolution (disconj failure p) + +disconjcomm :: TestTree +disconjcomm = testProperty "Commutative" + . forPred2 + $ \p o -> + hasSolution (disconj p o) ==> hasSolution (disconj o p) + +disconjassoc :: TestTree +disconjassoc = testProperty "Associative" + . forPred3 + $ \l m r -> + hasSolution (disconj (disconj l m) r) + ==> hasSolution (disconj l (disconj m r)) + +disconjTests :: TestTree +disconjTests = testGroup "Disconj" [disconjid, disconjcomm, disconjassoc] + +------------------------- Success -------------------------------------- +annihilatorDisconj :: TestTree +annihilatorDisconj = testProperty "Annihilates Disconj" + . forPred + $ \p -> hasSolution (disconj success p) + +successTests :: TestTree +successTests = testGroup "Success" [annihilatorDisconj] + +------------------------ Failure --------------------------------------- +annihilatorConj :: TestTree +annihilatorConj = testProperty "Annihilates Disconj" + . forPred + $ \p -> not $ hasSolution (conj failure p) + +failureTests :: TestTree +failureTests = testGroup "Success" [annihilatorConj] + +------------------------- Main ----------------------------------------- +main :: IO () +main = defaultMain . testGroup "List Tests" $ + [ eqTests + , neqTests + , freshTests + , conjTests + , disconjTests + , successTests + , failureTests ]