Type synonyms (#1865)

Adds type synonym declarations to the language, like so:
```
tydef Maybe a = Unit + a end
def lookdown : Cmd (Maybe Text) = scan down end

> lookdown
it2 : Maybe Text = inl ()
```

`tydef` behaves very similarly to `def` except that it defines a new (parameterized) type instead of a new term.

Note that higher-kinded types are not yet supported; for example we cannot say `tydef Foo f = Unit + f Int` (in fact this would be a syntax error since type variables cannot be at the head of an application).  However there is nothing stopping us from adding that in the future; I just wanted to keep things simple for now.

If you know of any scenario code that would be a good candidate for using type synonyms, let me know --- it would be nice to update a few scenarios as a better stress test of type synonyms before merging this.

Closes #153.

editors/emacs/swarm-mode.el

@@ -27,7 +27,7 @@
       (let* (
              ;; Generate the current keywords with:
              ;; cabal run swarm:swarm-docs -- editors --emacs
-             (x-keywords '("def" "end" "let" "in" "require"))
+             (x-keywords '("def" "tydef" "end" "let" "in" "require"))
              (x-builtins '(
                "self"
                "parent"

editors/vim/swarm.vim

@@ -1,4 +1,4 @@
-syn keyword Keyword def end let in require
+syn keyword Keyword def tydef 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/maybe.sw

@@ -0,0 +1,9 @@
+tydef Maybe a = Unit + a end
+
+def just : a -> Maybe a = inr end
+
+def nothing : Maybe a = inl () end
+
+def positive : Int -> Maybe Int = \x.
+  if (x > 0) {just x} {nothing}
+end

feedback.yaml

@@ -1,3 +1,4 @@
 loops:
+  build: cabal build -j -O0 all
   test: cabal test -j -O0 --test-show-details=direct swarm:swarm-integration swarm:swarm-unit
   unit: cabal test -j -O0 --test-show-details=direct swarm:swarm-unit

src/swarm-engine/Swarm/Game/CESK.hs

@@ -95,7 +95,6 @@ import Swarm.Language.Context
 import Swarm.Language.Module
 import Swarm.Language.Pipeline
 import Swarm.Language.Pretty
-import Swarm.Language.Requirement (ReqCtx)
 import Swarm.Language.Syntax
 import Swarm.Language.Types
 import Swarm.Language.Value as V
@@ -143,7 +142,7 @@ data Frame
     --   we should take the resulting 'Env' and add it to the robot's
     --   'Swarm.Game.Robot.robotEnv', along with adding this accompanying 'Ctx' and
     --   'ReqCtx' to the robot's 'Swarm.Game.Robot.robotCtx'.
-    FLoadEnv TCtx ReqCtx
+    FLoadEnv Contexts
   | -- | We were executing a definition; next we should take the resulting value
     --   and return a context binding the variable to the value.
     FDef Var
@@ -290,17 +289,17 @@ initMachine t e s = initMachine' t e s []
 
 -- | Like 'initMachine', but also take an explicit starting continuation.
 initMachine' :: ProcessedTerm -> Env -> Store -> Cont -> CESK
-initMachine' (ProcessedTerm (Module t' ctx) _ reqCtx) e s k =
+initMachine' (ProcessedTerm (Module t' ctx tydefs) _ reqCtx) e s k =
   case t' ^. sType of
     -- If the starting term has a command type...
     Forall _ (TyCmd _) ->
-      case ctx of
+      case (ctx, tydefs) of
         -- ...but doesn't contain any definitions, just create a machine
         -- that will evaluate it and then execute it.
-        Empty -> In t e s (FExec : k)
+        (Empty, Empty) -> In t e s (FExec : k)
         -- Or, if it does contain definitions, then load the resulting
         -- context after executing it.
-        _ -> In t e s (FExec : FLoadEnv ctx reqCtx : k)
+        _ -> In t e s (FExec : FLoadEnv (Contexts ctx reqCtx tydefs) : k)
     -- Otherwise, for a term with a non-command type, just
     -- create a machine to evaluate it.
     _ -> In t e s k
@@ -367,7 +366,7 @@ prettyFrame (FApp v) (p, inner) = (10, prettyPrec 10 (valueToTerm v) <+> pparens
 prettyFrame (FLet x t _) (_, inner) = (11, hsep ["let", pretty x, "=", inner, "in", ppr t])
 prettyFrame (FTry v) (p, inner) = (10, "try" <+> pparens (p < 11) inner <+> prettyPrec 11 (valueToTerm v))
 prettyFrame (FUnionEnv _) inner = prettyPrefix "∪·" inner
-prettyFrame (FLoadEnv _ _) inner = prettyPrefix "L·" inner
+prettyFrame (FLoadEnv {}) inner = prettyPrefix "L·" inner
 prettyFrame (FDef x) (_, inner) = (11, "def" <+> pretty x <+> "=" <+> inner <+> "end")
 prettyFrame FExec inner = prettyPrefix "E·" inner
 prettyFrame (FBind Nothing t _) (p, inner) = (0, pparens (p < 1) inner <+> ";" <+> ppr t)

src/swarm-engine/Swarm/Game/Robot/Context.hs

@@ -19,7 +19,7 @@ import Swarm.Game.CESK qualified as C
 import Swarm.Language.Context qualified as Ctx
 import Swarm.Language.Requirement (ReqCtx)
 import Swarm.Language.Typed (Typed (..))
-import Swarm.Language.Types (TCtx)
+import Swarm.Language.Types (TCtx, TDCtx)
 import Swarm.Language.Value as V
 
 -- | A record that stores the information
@@ -37,13 +37,15 @@ data RobotContext = RobotContext
   , _defStore :: C.Store
   -- ^ A store containing memory cells allocated to hold
   --   definitions.
+  , _tydefVals :: TDCtx
+  -- ^ Type synonym definitions.
   }
   deriving (Eq, Show, Generic, Ae.FromJSON, Ae.ToJSON)
 
 makeLenses ''RobotContext
 
 emptyRobotContext :: RobotContext
-emptyRobotContext = RobotContext Ctx.empty Ctx.empty Ctx.empty C.emptyStore
+emptyRobotContext = RobotContext Ctx.empty Ctx.empty Ctx.empty C.emptyStore Ctx.empty
 
 type instance Index RobotContext = Ctx.Var
 type instance IxValue RobotContext = Typed Value

src/swarm-engine/Swarm/Game/Scenario/Scoring/GenericMetrics.hs

@@ -9,6 +9,7 @@ import Data.Aeson
 import Data.Ord (Down (Down))
 import GHC.Generics (Generic)
 import Swarm.Util (maxOn)
+import Swarm.Util.JSON (optionsUntagged)
 
 -- | This is a subset of the "ScenarioStatus" type
 -- that excludes the "NotStarted" case.
@@ -17,17 +18,11 @@ data Progress
   | Completed
   deriving (Eq, Ord, Show, Read, Generic)
 
-untaggedJsonOptions :: Options
-untaggedJsonOptions =
-  defaultOptions
-    { sumEncoding = UntaggedValue
-    }
-
 instance FromJSON Progress where
-  parseJSON = genericParseJSON untaggedJsonOptions
+  parseJSON = genericParseJSON optionsUntagged
 
 instance ToJSON Progress where
-  toJSON = genericToJSON untaggedJsonOptions
+  toJSON = genericToJSON optionsUntagged
 
 data Metric a = Metric Progress a
   deriving (Eq, Ord, Show, Read, Generic, FromJSON, ToJSON)

src/swarm-engine/Swarm/Game/State.hs

@@ -133,9 +133,8 @@ import Swarm.Game.World qualified as W
 import Swarm.Game.World.Gen (Seed)
 import Swarm.Language.Capability (constCaps)
 import Swarm.Language.Context qualified as Ctx
-import Swarm.Language.Module (Module (Module))
-import Swarm.Language.Pipeline (ProcessedTerm (ProcessedTerm), processTermEither)
-import Swarm.Language.Syntax (SrcLoc (..), Syntax' (..), allConst)
+import Swarm.Language.Pipeline (ProcessedTerm, processTermEither, processedSyntax)
+import Swarm.Language.Syntax (SrcLoc (..), allConst, sLoc)
 import Swarm.Language.Typed (Typed (Typed))
 import Swarm.Language.Types
 import Swarm.Log
@@ -167,9 +166,10 @@ parseCodeFile ::
   m CodeToRun
 parseCodeFile filepath = do
   contents <- sendIO $ TIO.readFile filepath
-  pt@(ProcessedTerm (Module (Syntax' srcLoc _ _ _) _) _ _) <-
-    either (throwError . CustomFailure) return (processTermEither contents)
-  let strippedText = stripSrc srcLoc contents
+  pt <- either (throwError . CustomFailure) return (processTermEither contents)
+
+  let srcLoc = pt ^. processedSyntax . sLoc
+      strippedText = stripSrc srcLoc contents
       programBytestring = TL.encodeUtf8 $ TL.fromStrict strippedText
       sha1Hash = showDigest $ sha1 programBytestring
   return $ CodeToRun (PlayerAuthored filepath $ Sha1 sha1Hash) pt

src/swarm-engine/Swarm/Game/Step.hs

@@ -650,7 +650,8 @@ stepCESK cesk = case cesk of
   In tm@(TDef r x _ t) e s k -> withExceptions s k $ do
     hasCapabilityFor CEnv tm
     return $ Out (VDef r x t e) s k
-
+  -- Type definitions just turn into a no-op.
+  In (TTydef {}) e s k -> return $ In (TConst Noop) e s k
   -- Bind expressions don't evaluate: just package it up as a value
   -- until such time as it is to be executed.
   In (TBind mx t1 t2) e s k -> return $ Out (VBind mx t1 t2 e) s k
@@ -790,12 +791,17 @@ stepCESK cesk = case cesk of
   -- environment, store, and type and capability contexts into the robot's
   -- top-level environment and contexts, so they will be available to
   -- future programs.
-  Out (VResult v e) s (FLoadEnv ctx rctx : k) -> do
+  Out (VResult v e) s (FLoadEnv (Contexts ctx rctx tdctx) : k) -> do
     robotContext . defVals %= (`union` e)
     robotContext . defTypes %= (`union` ctx)
     robotContext . defReqs %= (`union` rctx)
+    robotContext . tydefVals %= (`union` tdctx)
+    return $ Out v s k
+  Out v s (FLoadEnv (Contexts ctx rctx tdctx) : k) -> do
+    robotContext . defTypes %= (`union` ctx)
+    robotContext . defReqs %= (`union` rctx)
+    robotContext . tydefVals %= (`union` tdctx)
     return $ Out v s k
-  Out v s (FLoadEnv {} : k) -> return $ Out v s k
   -- Any other type of value wiwth an FExec frame is an error (should
   -- never happen).
   Out _ s (FExec : _) -> badMachineState s "FExec frame with non-executable value"

src/swarm-engine/Swarm/Game/Step/Path/Type.hs

@@ -17,7 +17,7 @@
 module Swarm.Game.Step.Path.Type where
 
 import Control.Lens
-import Data.Aeson (Options (..), SumEncoding (ObjectWithSingleField), ToJSON (..), defaultOptions, genericToJSON)
+import Data.Aeson (ToJSON (..), genericToJSON)
 import Data.IntMap.Strict (IntMap)
 import Data.List.NonEmpty (NonEmpty)
 import Data.Map (Map)
@@ -28,6 +28,7 @@ import Swarm.Game.Location
 import Swarm.Game.Robot (RID)
 import Swarm.Game.Robot.Walk (WalkabilityContext)
 import Swarm.Game.Universe (SubworldName)
+import Swarm.Util.JSON (optionsObjectSingleField)
 import Swarm.Util.Lens (makeLensesNoSigs)
 import Swarm.Util.RingBuffer
 
@@ -67,19 +68,13 @@ data CacheLogEntry = CacheLogEntry
   }
   deriving (Show, Eq, Generic, ToJSON)
 
-objectSingleFieldEncoding :: Options
-objectSingleFieldEncoding =
-  defaultOptions
-    { sumEncoding = ObjectWithSingleField
-    }
-
 data CacheRetrievalAttempt
   = Success
   | RecomputationRequired CacheRetreivalInapplicability
   deriving (Show, Eq, Generic)
 
 instance ToJSON CacheRetrievalAttempt where
-  toJSON = genericToJSON objectSingleFieldEncoding
+  toJSON = genericToJSON optionsObjectSingleField
 
 -- | Certain events can obligate the cache to be
 -- completely invalidated, or partially or fully preserved.
@@ -90,7 +85,7 @@ data CacheEvent
   deriving (Show, Eq, Generic)
 
 instance ToJSON CacheEvent where
-  toJSON = genericToJSON objectSingleFieldEncoding
+  toJSON = genericToJSON optionsObjectSingleField
 
 data DistanceLimitChange
   = LimitIncreased
@@ -113,7 +108,7 @@ data CacheRetreivalInapplicability
   deriving (Show, Eq, Generic)
 
 instance ToJSON CacheRetreivalInapplicability where
-  toJSON = genericToJSON objectSingleFieldEncoding
+  toJSON = genericToJSON optionsObjectSingleField
 
 -- | Reasons for cache being invalidated
 data InvalidationReason

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

@@ -50,4 +50,6 @@ data UnificationError where
   Infinite :: IntVar -> UType -> UnificationError
   -- | Mismatch error between the given terms.
   UnifyErr :: TypeF UType -> TypeF UType -> UnificationError
+  -- | Encountered an undefined/unknown type constructor.
+  UndefinedUserType :: UType -> UnificationError
   deriving (Show)

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

@@ -23,6 +23,7 @@ import Control.Applicative (Alternative)
 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.State (State, get, gets, modify)
 import Control.Effect.Throw (Throw, throwError)
 import Control.Monad (zipWithM)
@@ -86,11 +87,6 @@ instance Substitutes IntVar UType UType where
 ------------------------------------------------------------
 -- Carrier type
 
--- Note: this carrier type and the runUnification function are
--- identical between this module and Swarm.Effect.Unify.Naive, but it
--- seemed best to duplicate it, so we can modify the carriers
--- independently in the future if we want.
-
 -- | Carrier type for unification: we maintain a current substitution,
 --   a counter for generating fresh unification variables, and can
 --   throw unification errors.
@@ -104,8 +100,13 @@ newtype UnificationC m a = UnificationC
 newtype FreshVarCounter = FreshVarCounter {getFreshVarCounter :: Int}
   deriving (Eq, Ord, Enum)
 
--- | Run a 'Unification' effect via the 'UnificationC' carrier.
-runUnification :: Algebra sig m => UnificationC m a -> m (Either UnificationError a)
+-- | Run a 'Unification' effect via the 'UnificationC' carrier.  Note
+--   that we also require an ambient @Reader 'TDCtx'@ effect, so unification
+--   will be sure to pick up whatever type aliases happen to be in scope.
+runUnification ::
+  (Algebra sig m, Has (Reader TDCtx) sig m) =>
+  UnificationC m a ->
+  m (Either UnificationError a)
 runUnification =
   unUnificationC >>> evalState idS >>> evalState (FreshVarCounter 0) >>> runThrow
 
@@ -132,7 +133,10 @@ runUnification =
 
 -- | Implementation of the 'Unification' effect in terms of the
 --   'UnificationC' carrier.
-instance Algebra sig m => Algebra (Unification :+: sig) (UnificationC m) where
+instance
+  (Algebra sig m, Has (Reader TDCtx) sig m) =>
+  Algebra (Unification :+: sig) (UnificationC m)
+  where
   alg hdl sig ctx = UnificationC $ case sig of
     L (Unify t1 t2) -> (<$ ctx) <$> runThrow (unify t1 t2)
     L (ApplyBindings t) -> do
@@ -152,6 +156,7 @@ instance Algebra sig m => Algebra (Unification :+: sig) (UnificationC m) where
 --   instead lazily during substitution.
 unify ::
   ( Has (Throw UnificationError) sig m
+  , Has (Reader TDCtx) sig m
   , Has (State (Subst IntVar UType)) sig m
   ) =>
   UType ->
@@ -165,13 +170,18 @@ unify ty1 ty2 = case (ty1, ty2) 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 a unification variable which /is not/ bound by the current
 --   substitution with another term.  If the other term is also a
 --   variable, we must look it up as well to see if it is bound.
 unifyVar ::
   ( Has (Throw UnificationError) sig m
+  , Has (Reader TDCtx) sig m
   , Has (State (Subst IntVar UType)) sig m
   ) =>
   IntVar ->
@@ -199,6 +209,7 @@ unifyVar x t = modify (insert x t) >> pure t
 --   contents.
 unifyF ::
   ( Has (Throw UnificationError) sig m
+  , Has (Reader TDCtx) sig m
   , Has (State (Subst IntVar UType)) sig m
   ) =>
   TypeF UType ->

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

@@ -11,7 +11,10 @@
 -- substitutions, and returns a substitution from unification which
 -- must then be composed with the substitution being tracked.
 --
--- Not used in Swarm, but useful for testing/comparison.
+-- 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
+-- testing/comparison.
 module Swarm.Effect.Unify.Naive where
 
 import Control.Algebra

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

@@ -8,7 +8,7 @@
 module Swarm.Language.Context where
 
 import Control.Algebra (Has)
-import Control.Effect.Reader (Reader, local)
+import Control.Effect.Reader (Reader, ask, local)
 import Control.Lens.Empty (AsEmpty (..))
 import Control.Lens.Prism (prism)
 import Data.Aeson (FromJSON, ToJSON)
@@ -53,6 +53,10 @@ singleton x t = Ctx (M.singleton x t)
 lookup :: Var -> Ctx t -> Maybe t
 lookup x (Ctx c) = M.lookup x c
 
+-- | Look up a variable in a context in an ambient Reader effect.
+lookupR :: Has (Reader (Ctx t)) sig m => Var -> m (Maybe t)
+lookupR x = lookup x <$> ask
+
 -- | Delete a variable from a context.
 delete :: Var -> Ctx t -> Ctx t
 delete x (Ctx c) = Ctx (M.delete x c)