Recursive types

editors/emacs/swarm-mode.el

@@ -154,7 +154,7 @@
   "Regexp that recognizes types (all uppercase strings are supposed to be types) in swarm language.")
 
 (defvar swarm-mode-keywords-regexp
-  (concat "\\b" (regexp-opt '("def" "tydef" "end" "let" "in" "require") t) "\\b")
+  (concat "\\b" (regexp-opt '("def" "tydef" "rec" "end" "let" "in" "require") t) "\\b")
   "Regexp that recognizes keywords in swarm language.")
 
 (defvar swarm-font-lock-keywords

editors/vim/swarm.vim

@@ -1,4 +1,4 @@
-syn keyword Keyword def tydef end let in require
+syn keyword Keyword def tydef rec end let in require
 syn keyword Builtins self parent base if inl inr case fst snd force undefined fail not format chars split charat tochar key
 syn keyword Command noop wait selfdestruct move backup volume path push stride turn grab harvest sow ignite place ping give equip unequip make has equipped count drill use build salvage reprogram say listen log view appear create halt time scout whereami waypoint structure floorplan hastag tagmembers detect resonate density sniff chirp watch surveil heading blocked scan upload ishere isempty meet meetall whoami setname random run return try swap atomic instant installkeyhandler teleport as robotnamed robotnumbered knows
 syn keyword Direction east north west south down forward left back right

example/omega.sw

@@ -0,0 +1,5 @@
+tydef D = rec d. d -> d end
+
+def selfApp : D -> D = \x. x x end
+
+def omega : D = selfApp selfApp end

example/rectypes.sw

@@ -0,0 +1,107 @@
+// 'rec t. F(t)' creates a recursive type which is the solution of t = F(t).
+// For example 'rec l. Unit + Int * l' is the type l such that l = Unit + Int * l,
+// that is, arbitrary-length finite lists of Int.
+//
+// Recursive types are equal up to alpha-renaming, so e.g.
+// (rec l. Unit + Int * l) = (rec q. Unit + Int * q)
+
+////////////////////////////////////////////////////////////
+// Lists
+////////////////////////////////////////////////////////////
+
+tydef List a = rec l. Unit + a * l end
+
+def nil : List a = inl () end
+def cons : a -> List a -> List a = \x. \l. inr (x, l) end
+
+def foldr : (a -> b -> b) -> b -> List a -> b = \f. \z. \xs.
+  case xs
+    (\_. z)
+    (\c. f (fst c) (foldr f z (snd c)))
+end
+
+def map : (a -> b) -> List a -> List b = \f.
+  foldr (\y. cons (f y)) nil
+end
+
+def append : List a -> List a -> List a = \xs. \ys.
+  foldr cons ys xs
+end
+
+def concat : List (List a) -> List a = foldr append nil end
+
+def sum : List Int -> Int =
+  foldr (\x. \y. x + y) 0
+end
+
+def twentySeven = sum (cons 12 (cons 5 (cons 3 (cons 7 nil)))) end
+
+// Note that if a function returns e.g. (rec t. Unit + (Int * Int) * t),
+// that is the *same type* as List (Int * Int), so we can use any List
+// functions on the output.
+
+def someFun : Int -> (rec t. Unit + (Int * Int) * t) = \x. inr ((x, x), inl ()) end
+
+def doSomethingWithSomeFun : List (Int * Int) =
+  (cons (2,3) (cons (4,7) (someFun 5)))
+end
+
+////////////////////////////////////////////////////////////
+// Binary trees with a at internal nodes and b at leaves
+////////////////////////////////////////////////////////////
+
+tydef BTree a b = rec bt. b + bt * a * bt end
+
+def leaf : b -> BTree a b = inl end
+
+def branch : BTree a b -> a -> BTree a b -> BTree a b =
+  \l. \a. \r. inr (l, a, r)
+end
+
+def foldBTree : (b -> c) -> (c -> a -> c -> c) -> BTree a b -> c =
+  \lf. \br. \t.
+    case t
+      lf
+      // fst p, fst (snd p), snd (snd p) is annoying; see #1893
+      (\p. br (foldBTree lf br (fst p)) (fst (snd p)) (foldBTree lf br (snd (snd p))))
+end
+
+def max : Int -> Int -> Int = \a. \b. if (a > b) {a} {b} end
+
+def height : BTree a b -> Int =
+  foldBTree (\_. 0) (\l. \_. \r. 1 + max l r)
+end
+
+////////////////////////////////////////////////////////////
+// Rose trees
+////////////////////////////////////////////////////////////
+
+// It would be better to reuse the definition of List
+// and define Rose a = rec r. a * List r,
+// but we do it this way just to show off nested rec
+tydef Rose a = rec r. a * (rec l. Unit + r * l) end
+
+def foldRose : (a -> List b -> b) -> Rose a -> b = \f. \r.
+  f (fst r) (map (foldRose f) (snd r))
+end
+
+def flatten : Rose a -> List a =
+  foldRose (\a. \ts. cons a (concat ts))
+end
+
+////////////////////////////////////////////////////////////
+// Equirecursive types
+////////////////////////////////////////////////////////////
+
+// Swarm has equirecursive types, which means a recursive type is
+// *equal to* its unfolding.  This has some interesting consequences
+// including the fact that types are equal if their infinite unfoldings
+// would be equal.
+
+// For example, U1 and U2 below are the same, and the Swarm
+// typechecker can tell:
+
+tydef U1 = rec u1. Unit + u1 end
+tydef U2 = rec u2. Unit + Unit + u2 end
+
+def u : U1 -> U2 = \u. u end

src/swarm-lang/Swarm/Effect/Unify.hs

@@ -52,4 +52,7 @@ data UnificationError where
   UnifyErr :: TypeF UType -> TypeF UType -> UnificationError
   -- | Encountered an undefined/unknown type constructor.
   UndefinedUserType :: UType -> UnificationError
+  -- | Encountered an unexpanded recursive type in unifyF.  This
+  --   should never happen.
+  UnexpandedRecTy :: TypeF UType -> UnificationError
   deriving (Show)

src/swarm-lang/Swarm/Effect/Unify/Fast.hs

@@ -20,18 +20,24 @@ module Swarm.Effect.Unify.Fast where
 
 import Control.Algebra
 import Control.Applicative (Alternative)
+import Control.Carrier.Accum.FixedStrict (AccumC, runAccum)
+import Control.Carrier.Reader (ReaderC, runReader)
 import Control.Carrier.State.Strict (StateC, evalState)
 import Control.Carrier.Throw.Either (ThrowC, runThrow)
 import Control.Category ((>>>))
-import Control.Effect.Reader (Reader)
+import Control.Effect.Accum (Accum, add)
+import Control.Effect.Reader (Reader, ask, local)
 import Control.Effect.State (State, get, gets, modify)
 import Control.Effect.Throw (Throw, throwError)
 import Control.Monad (zipWithM)
 import Control.Monad.Free
 import Control.Monad.Trans (MonadIO)
 import Data.Function (on)
+import Data.Functor.Identity
 import Data.Map qualified as M
 import Data.Map.Merge.Lazy qualified as M
+import Data.Monoid (First (..))
+import Data.Set (Set)
 import Data.Set qualified as S
 import Swarm.Effect.Unify
 import Swarm.Effect.Unify.Common
@@ -71,18 +77,44 @@ class Substitutes n b a where
 -- | We can perform substitution on terms built up as the free monad
 --   over a structure functor @f@.
 instance Substitutes IntVar UType UType where
-  subst s = go S.empty
+  subst s u = case runSubst (go u) of
+    -- If the substitution completed without encountering a repeated
+    -- variable, just return the result.
+    (First Nothing, u') -> return u'
+    -- Otherwise, throw an error, but re-run substitution starting at
+    -- the repeated variable to generate an expanded cyclic equality
+    -- constraint of the form x = ... x ... .
+    (First (Just x), _) ->
+      throwError $
+        Infinite x (snd (runSubst (go $ Pure x)))
    where
-    go seen (Pure x) = case lookup x s of
+    runSubst :: ReaderC (Set IntVar) (AccumC (First IntVar) Identity) a -> (First IntVar, a)
+    runSubst = run . runAccum (First Nothing) . runReader S.empty
+
+    -- A version of substitution that recurses through the term,
+    -- keeping track of unification variables seen along the current
+    -- path.  When it encounters a previously-seen variable, it simply
+    -- returns it unchanged but notes the first such variable that was
+    -- encountered.
+    go ::
+      (Has (Reader (Set IntVar)) sig m, Has (Accum (First IntVar)) sig m) =>
+      UType ->
+      m UType
+    go (Pure x) = case lookup x s of
       Nothing -> pure $ Pure x
-      Just t
-        | S.member x seen -> throwError $ Infinite x t
-        | otherwise -> go (S.insert x seen) t
-    go seen (Free t) = Free <$> goF seen t
+      Just t -> do
+        seen <- ask
+        case S.member x seen of
+          True -> add (First (Just x)) >> pure (Pure x)
+          False -> local (S.insert x) $ go t
+    go (Free t) = Free <$> goF t
 
-    goF seen (TyConF c ts) = TyConF c <$> mapM (go seen) ts
-    goF _ t@(TyVarF {}) = pure t
-    goF seen (TyRcdF m) = TyRcdF <$> mapM (go seen) m
+    goF :: (Has (Reader (Set IntVar)) sig m, Has (Accum (First IntVar)) sig m) => TypeF UType -> m (TypeF UType)
+    goF (TyConF c ts) = TyConF c <$> mapM go ts
+    goF t@(TyVarF {}) = pure t
+    goF (TyRcdF m) = TyRcdF <$> mapM go m
+    goF (TyRecF x t) = TyRecF x <$> go t
+    goF t@(TyRecVarF _) = pure t
 
 ------------------------------------------------------------
 -- Carrier type
@@ -92,7 +124,17 @@ instance Substitutes IntVar UType UType where
 --   throw unification errors.
 newtype UnificationC m a = UnificationC
   { unUnificationC ::
-      StateC (Subst IntVar UType) (StateC FreshVarCounter (ThrowC UnificationError m)) a
+      StateC
+        (Set (UType, UType))
+        ( StateC
+            (Subst IntVar UType)
+            ( StateC
+                FreshVarCounter
+                ( ThrowC UnificationError m
+                )
+            )
+        )
+        a
   }
   deriving newtype (Functor, Applicative, Alternative, Monad, MonadIO)
 
@@ -108,7 +150,11 @@ runUnification ::
   UnificationC m a ->
   m (Either UnificationError a)
 runUnification =
-  unUnificationC >>> evalState idS >>> evalState (FreshVarCounter 0) >>> runThrow
+  unUnificationC
+    >>> evalState S.empty
+    >>> evalState idS
+    >>> evalState (FreshVarCounter 0)
+    >>> runThrow
 
 ------------------------------------------------------------
 -- Unification
@@ -149,32 +195,68 @@ instance
     L (FreeUVars t) -> do
       s <- get @(Subst IntVar UType)
       (<$ ctx) . fuvs <$> subst s t
-    R other -> alg (unUnificationC . hdl) (R (R (R other))) ctx
+    R other -> alg (unUnificationC . hdl) (R (R (R (R other)))) ctx
 
 -- | Unify two types, returning a unified type equal to both.  Note
 --   that for efficiency we /don't/ do an occurs check here, but
 --   instead lazily during substitution.
+--
+--   We keep track of a set of pairs of types we have seen; if we ever
+--   see a pair a second time we simply assume they are equal without
+--   recursing further.  This constitutes a finite (coinductive)
+--   algorithm for doing unification on recursive types.
+--
+--   For example, suppose we wanted to unify @rec s. Unit + Unit + s@
+--   and @rec t. Unit + t@.  These types are actually equal since
+--   their infinite unfoldings are both @Unit + Unit + Unit + ...@ In
+--   practice we would proceed through the following recursive calls
+--   to unify:
+--
+--   @
+--     (rec s. Unit + Unit + s)                 =:= (rec t. Unit + t)
+--         { unfold the LHS }
+--     (Unit + Unit + (rec s. Unit + Unit + s)) =:= (rec t. Unit + t)
+--         { unfold the RHS }
+--     (Unit + Unit + (rec s. Unit + Unit + s)) =:= (Unit + (rec t. Unit + t)
+--         { unifyF matches the + and makes two calls to unify }
+--     Unit =:= Unit   { trivial}
+--     (Unit + (rec s. Unit + Unit + s))        =:= (rec t. Unit + t)
+--         { unfold the RHS }
+--     (Unit + (rec s. Unit + Unit + s))        =:= (Unit + (rec t. Unit + t))
+--         { unifyF on + }
+--     (rec s. Unit + Unit + s)                 =:= (rec t. Unit + t)
+--         { back to the starting pair, return success }
+--   @
 unify ::
   ( Has (Throw UnificationError) sig m
   , Has (Reader TDCtx) sig m
   , Has (State (Subst IntVar UType)) sig m
+  , Has (State (Set (UType, UType))) sig m
   ) =>
   UType ->
   UType ->
   m UType
-unify ty1 ty2 = case (ty1, ty2) of
-  (Pure x, Pure y) | x == y -> pure (Pure x)
-  (Pure x, y) -> do
-    mxv <- lookupS x
-    case mxv of
-      Nothing -> unifyVar x y
-      Just xv -> unify xv y
-  (x, Pure y) -> unify (Pure y) x
-  (UTyUser x1 tys, _) -> do
-    ty1' <- expandTydef x1 tys
-    unify ty1' ty2
-  (_, UTyUser {}) -> unify ty2 ty1
-  (Free t1, Free t2) -> Free <$> unifyF t1 t2
+unify ty1 ty2 = do
+  seen <- get @(Set (UType, UType))
+  case S.member (ty1, ty2) seen of
+    True -> return ty1
+    False -> do
+      modify (S.insert (ty1, ty2))
+      case (ty1, ty2) of
+        (Pure x, Pure y) | x == y -> pure (Pure x)
+        (Pure x, y) -> do
+          mxv <- lookupS x
+          case mxv of
+            Nothing -> unifyVar x y
+            Just xv -> unify xv y
+        (x, Pure y) -> unify (Pure y) x
+        (UTyRec x ty, _) -> unify (unfoldRec x ty) ty2
+        (_, UTyRec x ty) -> unify ty1 (unfoldRec x ty)
+        (UTyUser x1 tys, _) -> do
+          ty1' <- expandTydef x1 tys
+          unify ty1' ty2
+        (_, UTyUser {}) -> unify ty2 ty1
+        (Free t1, Free t2) -> Free <$> unifyF t1 t2
 
 -- | Unify a unification variable which /is not/ bound by the current
 --   substitution with another term.  If the other term is also a
@@ -183,6 +265,7 @@ unifyVar ::
   ( Has (Throw UnificationError) sig m
   , Has (Reader TDCtx) sig m
   , Has (State (Subst IntVar UType)) sig m
+  , Has (State (Set (UType, UType))) sig m
   ) =>
   IntVar ->
   UType ->
@@ -211,11 +294,18 @@ unifyF ::
   ( Has (Throw UnificationError) sig m
   , Has (Reader TDCtx) sig m
   , Has (State (Subst IntVar UType)) sig m
+  , Has (State (Set (UType, UType))) sig m
   ) =>
   TypeF UType ->
   TypeF UType ->
   m (TypeF UType)
 unifyF t1 t2 = case (t1, t2) of
+  -- Recursive types are always expanded in 'unify', these first four cases
+  -- should never happen.
+  (TyRecF {}, _) -> throwError $ UnexpandedRecTy t1
+  (_, TyRecF {}) -> throwError $ UnexpandedRecTy t2
+  (TyRecVarF {}, _) -> throwError $ UnexpandedRecTy t1
+  (_, TyRecVarF {}) -> throwError $ UnexpandedRecTy t2
   (TyConF c1 ts1, TyConF c2 ts2) -> case c1 == c2 of
     True -> TyConF c1 <$> zipWithM unify ts1 ts2
     False -> unifyErr

src/swarm-lang/Swarm/Effect/Unify/Naive.hs

@@ -13,7 +13,7 @@
 --
 -- Not used in Swarm, and also unmaintained
 -- (e.g. "Swarm.Effect.Unify.Fast" now supports expanding type
--- aliases; this module does not). It's still here just for
+-- aliases + recursive types; this module does not). It's still here just for
 -- testing/comparison.
 module Swarm.Effect.Unify.Naive where
 
@@ -164,5 +164,8 @@ unifyF t1 t2 = case (t1, t2) of
       False -> unifyErr
       _ -> (fmap compose . sequence) (M.merge M.dropMissing M.dropMissing (M.zipWithMatched (const unify)) m1 m2)
   (TyRcdF {}, _) -> unifyErr
+  -- Don't support any extra features (e.g. recursive types), so just
+  -- add a catch-all failure case
+  (_, _) -> unifyErr
  where
   unifyErr = throwError $ UnifyErr t1 t2

src/swarm-lang/Swarm/Language/Capability.hs

@@ -185,6 +185,8 @@ data Capability
     CHandleinput
   | -- | Capability to make other robots halt.
     CHalt
+  | -- | Capability to handle recursive types.
+    CRectype
   | -- | God-like capabilities.  For e.g. commands intended only for
     --   checking challenge mode win conditions, and not for use by
     --   players.