Now MkFree requires monadic instance

CHANGELOG.md

@@ -2,6 +2,11 @@
 
 ## version 0
 
+### 0.2 -- still not released
+
+* Now MkFree requires monadic instance.
+* Binder requires Monad typeclass.
+
 ### 0.1 -- 2023-10-04
 
 Initial release.

src/Data/Binder.hs

@@ -88,20 +88,20 @@ data Box m a
 
 -- | Typeclass for free variable constructor.
 class MkFree m a where
-  mkFree :: Var m a -> a
+  mkFree :: Var m a -> m a
 
 data AnyVar m = forall a. MkFree m a => AnyVar (Var m a)
 type EnvVar m = M.Map (Numbering m) (AnyVar m)
 data AnyMkFree m = forall a. MkFree m a => AnyMkFree a
 type EnvMkFree m = M.Map (Numbering m) (AnyMkFree m)
-newtype Closure m a = Closure { unClosure :: (EnvMkFree m) -> a }
+newtype Closure m a = Closure { unClosure :: (EnvMkFree m) -> m a }
 
-instance Functor (Closure m) where
-  fmap f cla = Closure $ f . unClosure cla
+instance Functor m => Functor (Closure m) where
+  fmap f cla = Closure $ fmap f . unClosure cla
 
-instance Applicative (Closure m) where
-  pure a = Closure $ const a
-  clf <*> cla = Closure $ \env -> unClosure clf env $ unClosure cla env
+instance Applicative m => Applicative (Closure m) where
+  pure a = Closure $ const $ pure a
+  clf <*> cla = Closure $ \env -> unClosure clf env <*> unClosure cla env
 
 instance MonadNumbering m => Eq (Var m a) where
   Var x _ == Var y _ = x == y
@@ -140,7 +140,7 @@ newVar name = do
   let x = let b = Box'Env
                 (M.singleton i $ AnyVar x)
                 (Closure $ \env ->
-                  let f (AnyMkFree y) = unsafeCoerce y
+                  let f (AnyMkFree y) = pure $ unsafeCoerce y
                    in f $ fromJust $ M.lookup i env)
            in Var i $ VarBody name b
   return x
@@ -157,7 +157,7 @@ occur _ (Box'Closed _) = False
 occur v (Box'Env vs _) = M.member (v ^. var'Key) vs
 
 
-instance Functor (Box m) where
+instance Functor m => Functor (Box m) where
   fmap f (Box'Closed a) = Box'Closed (f a)
   fmap f (Box'Env vs ta) = Box'Env vs (f <$> ta)
 
@@ -167,21 +167,21 @@ instance (MonadNumbering m) => Applicative (Box m) where
   Box'Closed f <*> Box'Env va ta = Box'Env va (f <$> ta)
   Box'Env vf tf <*> Box'Closed a = Box'Env vf (appClosure tf a)
    where
-    appClosure clf x = Closure $ \env -> unClosure clf env x
+    appClosure clf x = Closure $ \env -> unClosure clf env <*> pure x
   Box'Env vf tf <*> Box'Env va ta = Box'Env (M.union vf va) (tf <*> ta)
 
 -- | Pick out and complete the construction of @a@.
-unbox :: forall m a. Box m a -> a
-unbox (Box'Closed t) = t
-unbox (Box'Env env cl) = unClosure cl $ f <$> env
+unbox :: forall m a. Monad m => Box m a -> m a
+unbox (Box'Closed t) = pure t
+unbox (Box'Env env cl) = unClosure cl =<< traverse f env
  where
-  f (AnyVar x) = AnyMkFree @m $ mkFree x
+  f (AnyVar x) = AnyMkFree @m <$> mkFree x
 
 box :: MonadNumbering m => a -> Box m a
 box = pure
 apBox :: MonadNumbering m => Box m (a -> b) -> Box m a -> Box m b
 apBox = (<*>)
-boxApply :: (a -> b) -> Box m a -> Box m b
+boxApply :: Functor m => (a -> b) -> Box m a -> Box m b
 boxApply = fmap
 boxApply2 :: MonadNumbering m => (a -> b -> c) -> Box m a -> Box m b -> Box m c
 boxApply2 f ta tb = f <$> ta <*> tb
@@ -198,57 +198,60 @@ boxT = sequenceA
 
 
 -- | Variable binding.
---   Essentially, @Binder a b@ means @a -> b@.
-data Binder a b = Binder
+--   Essentially, @Binder a m b@ means @a -> m b@.
+data Binder a m b = Binder
   { _binder'Name :: Text
-  , _binder'Body :: a -> b
+  , _binder'Body :: a -> m b
   }
 
 $(makeLenses ''Binder)
 
 -- | Variable substitution.
-subst :: Binder a b -> a -> b
+subst :: Binder a m b -> a -> m b
 subst b = b ^. binder'Body
 
 -- | unbinding
-unbind :: (MkFree m a, MonadNumbering m) => Binder a b -> m (Var m a, b)
+unbind :: (MkFree m a, MonadNumbering m) => Binder a m b -> m (Var m a, b)
 unbind b = do
   x <- newVar $ b ^. binder'Name
-  return (x, subst b $ mkFree x)
+  y <- subst b =<< mkFree x
+  return (x, y)
 
 unbind2 :: (MkFree m a, MonadNumbering m)
-        => Binder a b1 -> Binder a b2 -> m (Var m a, b1, b2)
+        => Binder a m b1 -> Binder a m b2 -> m (Var m a, b1, b2)
 unbind2 b1 b2 = do
   x <- newVar $ b1 ^. binder'Name
   let v = mkFree x
-  return (x, subst b1 v, subst b2 v)
+  y1 <- subst b1 =<< v
+  y2 <- subst b2 =<< v
+  return (x, y1, y2)
 
 -- | Check if two bindings are equal.
 eqBinder :: (MkFree m a, MonadNumbering m)
-         => (b -> b -> m Bool) -> Binder a b -> Binder a b -> m Bool
+         => (b -> b -> m Bool) -> Binder a m b -> Binder a m b -> m Bool
 eqBinder eq f g = do
   (_, t, u) <- unbind2 f g
   eq t u
 
 
 -- | Smart constructor for 'Binder'.
-buildBinder :: Var m a -> (a -> b) -> Binder a b
+buildBinder :: Var m a -> (a -> m b) -> Binder a m b
 buildBinder x body = Binder (x ^. var'Name) body
 
 -- | binding
 bind :: (MkFree m a, MonadNumbering m)
-        => Var m a -> Box m b -> Box m (Binder a b)
-bind x (Box'Closed t) = Box'Closed $ buildBinder x $ const t
+        => Var m a -> Box m b -> Box m (Binder a m b)
+bind x (Box'Closed t) = Box'Closed $ buildBinder x $ const $ return t
 bind x (Box'Env vs t) =
   let vs' = M.delete (x ^. var'Key) vs in if length vs' == 0
     then Box'Closed $ buildBinder x $
       \arg -> unClosure t $ M.singleton (x ^. var'Key) (AnyMkFree arg)
     else Box'Env vs' $ Closure $
-      \ms -> buildBinder x $
+      \ms -> return $ buildBinder x $
       \arg -> unClosure t $ M.insert (x ^. var'Key) (AnyMkFree arg) ms
 
 boxBinder :: (MkFree m a, MonadNumbering m)
-          => (b -> m (Box m b)) -> Binder a b -> m (Box m (Binder a b))
+          => (b -> m (Box m b)) -> Binder a m b -> m (Box m (Binder a m b))
 boxBinder f b = do
   (x, t) <- unbind b
   ft <- f t

test/Binder1Spec.hs

@@ -37,15 +37,15 @@ instance MonadNumbering S where
 
 data Term
   = Term'Var (Var S Term)
-  | Term'Abs (Binder Term Term)
+  | Term'Abs (Binder Term S Term)
   | Term'App Term Term
 
 instance MkFree S Term where
-  mkFree = Term'Var
+  mkFree = return . Term'Var
 
 var :: Var S Term -> Box S Term
 var = boxVar
-absRaw :: Box S (Binder Term Term) -> Box S Term
+absRaw :: Box S (Binder Term S Term) -> Box S Term
 absRaw = fmap Term'Abs
 abs :: Var S Term -> Box S Term -> Box S Term
 abs x t = absRaw $ bind x t
@@ -56,11 +56,13 @@ boxTerm (Term'Var x) = return $ var x
 boxTerm (Term'Abs b) = absRaw <$> boxBinder boxTerm b
 boxTerm (Term'App t u) = app <$> boxTerm t <*> boxTerm u
 
-eval :: Term -> Term
-eval t@(Term'App f a) = case eval f of
-  Term'Abs b -> eval (subst b a)
-  _ -> t
-eval t = t
+eval :: Term -> S Term
+eval t@(Term'App f a) = do
+  ef <- eval f
+  case ef of
+    Term'Abs b -> eval =<< subst b a
+    _ -> return t
+eval t = return t
 
 size :: Term -> S Int
 size (Term'Var _) = return 0
@@ -87,17 +89,17 @@ showTerm (Term'App t u) = do
 termIdentity, termFst, termDelta, termOmega :: S Term
 termIdentity = do
   x <- newVar "x"
-  return $ unbox $ abs x $ var x
+  unbox $ abs x $ var x
 termFst = do
   x <- newVar "x"
   y <- newVar "y"
-  return $ unbox $ abs x $ abs y $ var x
+  unbox $ abs x $ abs y $ var x
 termDelta = do
   x <- newVar "x"
-  return $ unbox $ abs x $ app (var x) (var x)
+  unbox $ abs x $ app (var x) (var x)
 termOmega = do
   delta <- box <$> termDelta
-  return $ unbox $ app delta delta
+  unbox $ app delta delta
 
 spec :: Spec
 spec = do

test/Binder2Spec.hs

@@ -39,38 +39,38 @@ instance MonadNumbering S where
 data Ty
   = Ty'Var (Var S Ty)
   | Ty'Arr Ty Ty
-  | Ty'All (Binder Ty Ty)
+  | Ty'All (Binder Ty S Ty)
 
 data Te
   = Te'Var (Var S Te)
-  | Te'Abs Ty (Binder Te Te)
+  | Te'Abs Ty (Binder Te S Te)
   | Te'App Te Te
-  | Te'Lam (Binder Ty Te)
+  | Te'Lam (Binder Ty S Te)
   | Te'Spe Te Ty
 
 instance MkFree S Ty where
-  mkFree = Ty'Var
+  mkFree = return . Ty'Var
 instance MkFree S Te where
-  mkFree = Te'Var
+  mkFree = return . Te'Var
 
 ty'Var :: Var S Ty -> Box S Ty
 ty'Var = boxVar
 ty'Arr :: Box S Ty -> Box S Ty -> Box S Ty
 ty'Arr a b = Ty'Arr <$> a <*> b
-ty'AllRaw :: Box S (Binder Ty Ty) -> Box S Ty
+ty'AllRaw :: Box S (Binder Ty S Ty) -> Box S Ty
 ty'AllRaw = fmap Ty'All
 ty'All :: Var S Ty -> Box S Ty -> Box S Ty
 ty'All x t = ty'AllRaw $ bind x t
 
 te'Var :: Var S Te -> Box S Te
 te'Var = boxVar
-te'AbsRaw :: Box S Ty -> Box S (Binder Te Te) -> Box S Te
+te'AbsRaw :: Box S Ty -> Box S (Binder Te S Te) -> Box S Te
 te'AbsRaw a f = Te'Abs <$> a <*> f
 te'Abs :: Box S Ty -> Var S Te -> Box S Te -> Box S Te
 te'Abs a x t = te'AbsRaw a $ bind x t
 te'App :: Box S Te -> Box S Te -> Box S Te
 te'App t u = Te'App <$> t <*> u
-te'LamRaw :: Box S (Binder Ty Te) -> Box S Te
+te'LamRaw :: Box S (Binder Ty S Te) -> Box S Te
 te'LamRaw = fmap Te'Lam
 te'Lam :: Var S Ty -> Box S Te -> Box S Te
 te'Lam x t = te'LamRaw $ bind x t
@@ -88,36 +88,41 @@ boxTe (Te'App t u) = te'App <$> boxTe t <*> boxTe u
 boxTe (Te'Lam f) = te'LamRaw <$> boxBinder boxTe f
 boxTe (Te'Spe t a) = te'Spe <$> boxTe t <*> boxTy a
 
-hnf :: Te -> Te
-hnf (Te'App t u) = let v = hnf u in case hnf t of
-  Te'Abs _ b -> hnf $ subst b v
-  h -> Te'App h v
-hnf (Te'Spe t a) = case hnf t of
-  Te'Lam b -> hnf $ subst b a
-  h -> Te'Spe h a
-hnf t = t
+hnf :: Te -> S Te
+hnf (Te'App t u) = do
+  hu <- hnf u
+  ht <- hnf t
+  case ht of
+    Te'Abs _ b -> hnf =<< subst b hu
+    _ -> return $ Te'App ht hu
+hnf (Te'Spe t a) = do
+  ht <- hnf t
+  case ht of
+    Te'Lam b -> hnf =<< subst b a
+    _ -> return $ Te'Spe ht a
+hnf t = return t
 
 nf :: Te -> S Te
 nf (Te'Abs a f) = do
   (x, t) <- unbind f
   nt <- nf t
   bt <- boxTe nt
-  return $ Te'Abs a $ unbox $ bind x bt
+  fmap (Te'Abs a) $ unbox $ bind x bt
 nf (Te'App t u) = do
   nt <- nf t
   nu <- nf u
   case nt of
-    Te'Abs _ f -> nf $ subst f u
+    Te'Abs _ f -> nf =<< subst f u
     _ -> return $ Te'App nt nu
 nf (Te'Lam f) = do
   (x, t) <- unbind f
   nt <- nf t
   bt <- boxTe nt
-  return $ Te'Lam $ unbox $ bind x bt
+  fmap Te'Lam $ unbox $ bind x bt
 nf (Te'Spe t a) = do
   nt <- nf t
   case nt of
-    Te'Lam f -> nf $ subst f a
+    Te'Lam f -> nf =<< subst f a
     _ -> return $ Te'Spe nt a
 nf t = return t
 
@@ -155,12 +160,12 @@ infer ctxt (Te'Lam f) = do
   case mtyt of
     Just tyt -> do
       bt <- boxTy tyt
-      return $ Just $ Ty'All $ unbox $ bind x bt
+      fmap (Just . Ty'All) $ unbox $ bind x bt
     Nothing -> return Nothing
 infer ctxt (Te'Spe t a) = do
   mtyt <- infer ctxt t
   case mtyt of
-    Just (Ty'All f) -> return $ Just $ subst f a
+    Just (Ty'All f) -> Just <$> subst f a
     _ -> return Nothing
 
 check :: Ctxt -> Te -> Ty -> S Bool
@@ -206,19 +211,19 @@ term1 :: S Te
 type1 = do
   x <- newVar "X"
   y <- newVar "Y"
-  return $ unbox $ ty'Arr (ty'Var x) (ty'Var y)
+  unbox $ ty'Arr (ty'Var x) (ty'Var y)
 type2 = do
   x <- newVar "X"
   y <- newVar "Y"
   let arr = ty'Arr (ty'Var x) (ty'Var y)
-  return $ unbox $ ty'All x $ ty'All y $ ty'Arr arr arr
+  unbox $ ty'All x $ ty'All y $ ty'Arr arr arr
 term1 = do
   x <- newVar "X"
   y <- newVar "Y"
   f <- newVar "f"
   a <- newVar "a"
   let arr = ty'Arr (ty'Var x) (ty'Var y)
-  return $ unbox $ te'Lam x $ te'Lam y $ te'Abs arr f $ te'Abs (ty'Var x) a $
+  unbox $ te'Lam x $ te'Lam y $ te'Abs arr f $ te'Abs (ty'Var x) a $
     te'App (te'Var f) (te'Var a)
 
 spec :: Spec