user-defined types

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)
@@ -105,7 +106,10 @@ 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)
+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 +136,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 +159,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 +173,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 +212,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/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)
 

src/swarm-lang/Swarm/Language/Parser/Lex.hs

@@ -34,6 +34,7 @@ module Swarm.Language.Parser.Lex (
   locTyName,
   identifier,
   tyVar,
+  tyName,
   tmVar,
   textLiteral,
   integer,
@@ -211,14 +212,14 @@ locIdentifier idTy = do
           failT ["reserved word", squote t, "cannot be used as variable name"]
       | otherwise -> return t
     SwarmLangLatest
-      | t `S.member` reservedWords || T.toLower t `S.member` reservedWords ->
-          failT ["Reserved word", squote t, "cannot be used as a variable name"]
       | IDTyVar <- idTy
       , T.toTitle t `S.member` reservedWords ->
           failT ["Reserved type name", squote t, "cannot be used as a type variable name; perhaps you meant", squote (T.toTitle t) <> "?"]
       | IDTyName <- idTy
-      , T.toTitle t `S.member` reservedWords ->
+      , t `S.member` reservedWords ->
           failT ["Reserved type name", squote t, "cannot be redefined."]
+      | t `S.member` reservedWords || T.toLower t `S.member` reservedWords ->
+          failT ["Reserved word", squote t, "cannot be used as a variable name"]
       | IDTyName <- idTy
       , isLower (T.head t) ->
           failT ["Type synonym names must start with an uppercase letter"]
@@ -248,6 +249,11 @@ identifier = fmap lvVar . locIdentifier
 tyVar :: Parser Var
 tyVar = identifier IDTyVar
 
+-- | Parse a (user-defined) type constructor name, which must start
+--   with an uppercase letter.
+tyName :: Parser Var
+tyName = identifier IDTyName
+
 -- | Parse a term variable, which can start in any case and just
 --   cannot be the same (case-insensitively) as a lowercase reserved
 --   word.