user-defined types

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

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,18 +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 _tydefs) _ 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)
-        -- XXX do we also need to load tydefs?
+        (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
@@ -368,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/Step.hs

@@ -791,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)

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

@@ -9,19 +9,21 @@ module Swarm.Language.Kindcheck (
 ) where
 
 import Control.Algebra (Has)
+import Control.Effect.Reader (Reader, ask)
 import Control.Effect.Throw (Throw, throwError)
 import Data.Fix (Fix (..))
-import Swarm.Language.Types (Poly (..), Polytype, TyCon, Type, TypeF (..), getArity, tcArity)
+import Swarm.Language.Types
 
 -- | Kind checking errors that can occur.  For now, the only possible
 --   error is an arity mismatch error.
 data KindError
-  = ArityMismatch TyCon [Type]
+  = ArityMismatch TyCon Int [Type]
+  | UndefinedTyCon TyCon Type
   deriving (Eq, Show)
 
 -- | Check that a polytype is well-kinded.
-checkPolytypeKind :: Has (Throw KindError) sig m => Polytype -> m ()
-checkPolytypeKind (Forall _ t) = checkKind t
+checkPolytypeKind :: (Has (Reader TDCtx) sig m, Has (Throw KindError) sig m) => Polytype -> m TydefInfo
+checkPolytypeKind pty@(Forall xs t) = TydefInfo pty (Arity $ length xs) <$ checkKind t
 
 -- | Check that a type is well-kinded. For now, we don't allow
 --   higher-kinded types, *i.e.* all kinds will be of the form @Type
@@ -32,9 +34,13 @@ checkPolytypeKind (Forall _ t) = checkKind t
 --   well want to generalize to arbitrary higher kinds (e.g. @(Type ->
 --   Type) -> Type@ etc.) which would require generalizing this
 --   checking code a bit.
-checkKind :: Has (Throw KindError) sig m => Type -> m ()
-checkKind (Fix (TyConF c tys)) = case compare (length tys) (getArity (tcArity c)) of
-  EQ -> mapM_ checkKind tys
-  _ -> throwError $ ArityMismatch c tys
+checkKind :: (Has (Reader TDCtx) sig m, Has (Throw KindError) sig m) => Type -> m ()
+checkKind ty@(Fix (TyConF c tys)) = do
+  tdCtx <- ask
+  case getArity <$> tcArity tdCtx c of
+    Nothing -> throwError $ UndefinedTyCon c ty
+    Just a -> case compare (length tys) a of
+      EQ -> mapM_ checkKind tys
+      _ -> throwError $ ArityMismatch c a tys
 checkKind (Fix (TyVarF _)) = return ()
 checkKind (Fix (TyRcdF m)) = mapM_ checkKind m

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

@@ -89,7 +89,7 @@ validateSwarmCode doc version content = do
           VU.Usage _ problems = VU.getUsage mempty term
           unusedWarnings = mapMaybe (VU.toErrPos content) problems
 
-          parsingErrors = case processParsedTerm' mempty mempty term of
+          parsingErrors = case processParsedTerm' mempty term of
             Right _ -> []
             Left e -> pure $ showTypeErrorPos content e
         Left e -> (pure $ showErrorPos e, [])

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

@@ -22,7 +22,7 @@ import Data.Yaml (FromJSON, ToJSON)
 import GHC.Generics (Generic)
 import Swarm.Language.Context (Ctx, empty)
 import Swarm.Language.Syntax (Syntax')
-import Swarm.Language.Types (Polytype, UPolytype, UType)
+import Swarm.Language.Types (Polytype, TDCtx, UPolytype, UType)
 
 ------------------------------------------------------------
 -- Modules
@@ -37,7 +37,7 @@ import Swarm.Language.Types (Polytype, UPolytype, UType)
 data Module s t = Module
   { _moduleSyntax :: Syntax' s
   , _moduleCtx :: Ctx t
-  , _moduleTydefs :: Ctx Polytype
+  , _moduleTydefs :: TDCtx
   }
   deriving (Show, Eq, Functor, Data, Generic, FromJSON, ToJSON)