Extract UnifyT into its own package and get an example going

packages.dhall

@@ -106,3 +106,7 @@ in  upstream
     with logict.repo = "https://dev.danilafe.com/Everything-I-Know-About-Types/logict.git"
     with logict.version = "24298710fa940bfcf2d272bc6d5c7417f2bfccfe"
     with logict.dependencies = [ "control", "lists", "maybe", "prelude", "transformers", "tuples" ]
+    with unifyt.repo = "https://dev.danilafe.com/Everything-I-Know-About-Types/unifyt.git"
+    with unifyt.version = "d1e227dbed5e5af63510872b95a9417200c0d7c7"
+    with unifyt.dependencies = [ "control", "foldable-traversable", "lazy", "maybe", "newtype", "ordered-collections", "prelude", "transformers", "tuples" ]
+

spago.dhall

@@ -24,6 +24,7 @@ to generate this file without the comments in this block.
   , "prelude"
   , "transformers"
   , "tuples"
+  , "unifyt"
   ]
 , packages = ./packages.dhall
 , sources = [ "src/**/*.purs", "test/**/*.purs" ]

src/Language/Bergamot/Syntax.purs

@@ -13,6 +13,9 @@ import Control.Applicative (class Applicative, pure)
 import Control.Bind (class Bind, bind, (>>=))
 import Control.MonadPlus (class MonadPlus)
 import Control.Monad.Logic.Class (class MonadLogic, msplit, interleave)
+import Control.Monad.Unify.Class (class MonadUnify, class Unifiable, class UnificationVariable, Stream(..), squash, alongside, ComparisonAction(..))
+import Control.Monad.Unify.Trans (UnifyT(..), runUnifyT)
+import Control.Monad.Logic.Trans (SFKT(..), runSFKT)
 import Data.List (List(..), (:))
 import Data.Functor (class Functor, (<$>), map)
 import Data.Eq (class Eq)
@@ -53,14 +56,6 @@ instance Traversable Expr where
 
     traverse f e = sequence (f <$> e)
 
-data Stream k = StreamCons k (Lazy (Stream k))
-
-pop :: forall k. Stream k -> Tuple k (Stream k)
-pop (StreamCons k lks) = Tuple k (force lks)
-
-class Ord k <= UnificationVariable k where
-    variables :: Stream k
-
 newtype IntVar = MkIntVar Int
 
 derive instance Eq IntVar
@@ -70,16 +65,6 @@ instance UnificationVariable IntVar where
     variables = mkVarList 0
         where mkVarList n = StreamCons (MkIntVar n) $ defer $ \_ -> mkVarList (n+1)
 
-data ComparisonAction k f
-    = Merge k k
-    | Store k (f k)
-    | Fail
-
-class (UnificationVariable k, Traversable f) <= Unifiable k f where
-    variable :: k -> f k
-    squash :: f (f k) -> f k
-    alongside :: f k -> f k -> f (ComparisonAction k f)
-
 instance UnificationVariable k => Unifiable k Expr where
     variable = Var
     squash (Var f) = f
@@ -95,93 +80,22 @@ instance UnificationVariable k => Unifiable k Expr where
           combine Nil (_:_) = (Var Fail) : Nil
           combine (x:xs) (y:ys) = alongside x y : combine xs ys
 
-class (Unifiable k f, MonadPlus m) <= MonadUnify k f m | m -> k, m -> f where
-    fresh :: m k
-    merge :: k -> k -> m Unit
-    store :: k -> f k -> m Unit
-    reify :: f k -> m (f k)
+newtype Unifier a = MkUnifier (UnifyT IntVar Expr (SFKT Maybe) a)
 
-unify :: forall k f m. MonadUnify k f m => f k -> f k -> m Unit
-unify f1 f2 =
-    do
-       _ <- traverse process $ alongside f1 f2
-       pure unit
-    where
-      process (Merge k1 k2) = merge k1 k2
-      process (Store k f) = store k f
-      process Fail = empty
+derive instance Newtype (Unifier a) _
+derive newtype instance Functor Unifier
+derive newtype instance Apply Unifier
+derive newtype instance Applicative Unifier
+derive newtype instance Alternative Unifier
+derive newtype instance Bind Unifier
+derive newtype instance Monad Unifier
+derive newtype instance MonadPlus Unifier
+derive newtype instance MonadUnify IntVar Expr Unifier
 
-type UnificationState k f =
-    { boundVariables :: Map k { equivalence :: Set k, boundTo :: Maybe (f k) }
-    , currentVariables :: Stream k
-    }
+-- >:(
+instance MonadLogic Unifier where
+    msplit m = MkUnifier $ MkUnifyT $ map (map (rmap (MkUnifier <<< MkUnifyT))) $ msplit $ un MkUnifyT $ un MkUnifier m
+    interleave = over2 MkUnifier (over2 MkUnifyT interleave)
 
-newtype UnifyT k f m a = MkUnifyT (StateT (UnificationState k f) m a)
-
-derive instance Newtype (UnifyT k f m a) _
-derive instance Functor m => Functor (UnifyT k f m)
-
-instance Monad m => Apply (UnifyT k f m) where
-    apply m1 m2 = MkUnifyT $ apply (un MkUnifyT m1) (un MkUnifyT m2)
-
-instance Monad m => Applicative (UnifyT k f m) where
-    pure a = MkUnifyT $ pure a
-
-instance Monad m => Bind (UnifyT k f m) where
-    bind m f = MkUnifyT $ (un MkUnifyT m) >>= (un MkUnifyT <<< f)
-
-instance Monad m => Monad (UnifyT k f m)
-
-instance (Monad m, Alt m) => Alt (UnifyT k f m) where
-    alt = over2 MkUnifyT alt
-
-instance (Monad m, Plus m) => Plus (UnifyT k f m) where
-    empty = MkUnifyT empty
-
-instance (Monad m, Alternative m) => Alternative (UnifyT k f m)
-instance (MonadPlus m) => MonadPlus (UnifyT k f m)
-
-instance MonadLogic m => MonadLogic (UnifyT k f m) where
-    msplit m = MkUnifyT $ map (map (rmap MkUnifyT)) $ msplit $ un MkUnifyT m
-    interleave m1 m2 = over2 MkUnifyT interleave m1 m2
-
-instance (Unifiable k f, MonadPlus m) => MonadUnify k f (UnifyT k f m) where
-    fresh = MkUnifyT $ do
-        Tuple k restVariables <- gets (pop <<< _.currentVariables)
-        _ <- modify $ _ { currentVariables = restVariables }
-        pure k
-    merge k1 k2 = do
-        boundVariables <- MkUnifyT $ gets _.boundVariables
-        let
-            equivalence k = fromMaybe (singleton k) (_.equivalence <$> lookup k boundVariables)
-            boundTo k = lookup k boundVariables >>= _.boundTo
-            fullSet = equivalence k1 `union` equivalence k2
-        newTerm <-
-            case boundTo k1 /\ boundTo k2 of
-                Just t1 /\ Just t2 -> unify t1 t2 >>= const (Just <$> reify t1)
-                Just t1 /\ Nothing -> pure $ Just t1
-                Nothing /\ Just t2 -> pure $ Just t2
-                Nothing /\ Nothing -> pure $ Nothing
-        let newMapValue = {equivalence: fullSet, boundTo: newTerm}
-        _ <- MkUnifyT $ modify $ _ { boundVariables = foldr (flip insert newMapValue) boundVariables fullSet }
-        pure unit
-    store k f = do
-        boundVariables <- MkUnifyT $ gets _.boundVariables
-        let fullSet = fromMaybe (singleton k) (_.equivalence <$> lookup k boundVariables)
-        let anyBound = any (isJust <<< (_>>=(_.boundTo)) <<< (flip lookup boundVariables)) fullSet
-        if anyBound
-            then empty
-            else do
-                let newMapValue = {equivalence: fullSet, boundTo: Just f}
-                _ <- MkUnifyT $ modify $ _ { boundVariables = foldr (flip insert newMapValue) boundVariables fullSet }
-                pure unit
-    reify f =
-        MkUnifyT $ do
-            boundVariables <- gets _.boundVariables
-            let
-                reify' f' = squash $ process <$> f'
-                process k = fromMaybe (variable k) (reify' <$> (lookup k boundVariables >>= _.boundTo))
-            pure $ reify' f
-
-runUnifyT :: forall k f m a. Monad m => UnificationVariable k => UnifyT k f m a -> m a
-runUnifyT m = fst <$> runStateT (un MkUnifyT m) { boundVariables: Map.empty, currentVariables: variables }
+runUnifier :: forall a. Unifier a -> Maybe a
+runUnifier m = runSFKT (runUnifyT $ un MkUnifier m) (const <<< Just) Nothing

test/Main.purs

@@ -1,6 +1,23 @@
 module Test.Main where
 
 import Prelude
+import Language.Bergamot.Syntax
+import Control.Monad.Logic.Trans
+import Control.Monad.Logic.Class
+import Control.Monad.Unify.Trans
+import Control.Monad.Unify.Class
+import Data.List
+import Data.Maybe
 
-main :: Unit
-main = unit
+runSomeComputation :: forall m. MonadLogic m => MonadUnify IntVar Expr m => m (Expr IntVar)
+runSomeComputation = do
+    x1 <- fresh
+    x2 <- fresh
+    let binPred = Atom "hello" $ fromFoldable [variable x1, variable x2]
+    let realBinPred = Atom "hello" $ fromFoldable [Atom "first" $ fromFoldable [], Atom "second" $ fromFoldable []]
+    unify binPred realBinPred
+    (unify (variable x1) (variable x2) >>= const (reify (variable x1))) `interleave` (unify (variable x1) (variable x1) >>= const (reify (variable x2)))
+    
+
+main :: Maybe (Expr IntVar)
+main = runUnifier runSomeComputation