New read command to act as partial inverse to format (#2224)

Towards #116.  This PR introduces a new built-in command `read`, which can (attempt to) convert text into values, *i.e.* a partial inverse to `format`.

It has type `read : Text -> a` and is a little bit magical, since its behavior depends on the inferred output type.  In particular, if reading at the expected output type succeeds, it will return the value read; otherwise it throws an exception.  In other words, in order to use `read` successfully you must already know what type you expect to get.

At first I gave it the type `Text -> (Unit + a)` and had it return `inl ()` whenever it failed, but then I realized that (1) you can make either version from the other (to convert `Text -> (Unit + a)` to `Text -> a`, `case` on the result and call `fail` if you get `inl`; to convert the other way, use `try`), but (2) it is simpler/easier to have the version that crashes to start and then use a `net` to turn it into the pure functional version if you wish, rather than the other way around (which requires a much harder-to-obtain `ADT calculator`).

From a technical point of view, the way this is achieved is by inserting the type inferred for `read` as an extra parameter during elaboration.  (Having types-as-special-values in the language might be useful for other things down the road as well.)  Note that this makes `read` strictly weaker than the `read` function in Haskell, which works via dictionary-passing.  For `read` in Swarm to work, its concrete type must be statically known at compile time.  For example here is a function that works in Haskell but not Swarm:
```
def testRead : a -> Bool = \x. read (format x) == x end
```
I think it should still be sufficiently usable, however, and the current implementation is much simpler than going to full-fledged type classes.

Currently `read` does not work on functions or delay types (even though such things are supported by `format`).  We may add them in the future, but it would be much more complex since it would require parsing arbitrary Swarm code and dealing properly with environments and closures etc.

`read` also does not currently work with user-defined types; see #2223 .

data/entities.yaml

@@ -330,6 +330,22 @@
     ignition: 0.1
     duration: [20, 40]
     product: ash
+- name: parsley
+  display:
+    attr: plant
+    char: 'p'
+  description:
+    - A fast-growing plant with a pungent aroma, often found growing near rocks.
+    - |
+      When equipped as a device, parsley enables the `read` command, which can be used to turn text into values:
+      ```
+      read : Text -> a
+      ```
+      If the given `Text`{=type} represents a value of the expected type, the value will be returned; otherwise, an exception is thrown.  For example, `(read "3" : Int) == 3`, but `read "hello" : Int` crashes.
+    - Note that `read`, unlike `format`, is unable to deal with function, delay, or command types.
+  properties: [pickable, growable]
+  capabilities: [read]
+  growth: [10, 100]
 - name: linotype
   display:
     attr: silver

data/worlds/classic.world

@@ -75,6 +75,7 @@ overlay
     [ {stone}
     , mask (hash % 10 == 0) {stone, rock}
     , mask (hash % 100 == 0) {stone, lodestone}
+    , mask (hash % 300 == 0) {grass, parsley}
     ]
   )
 , mask (big && soft && natural)

editors/emacs/swarm-mode.el

@@ -161,6 +161,7 @@
       "fail"
       "not"
       "format"
+      "read"
       "chars"
       "split"
       "charat"

editors/vim/swarm.vim

@@ -1,5 +1,5 @@
 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 Builtins self parent base if inl inr case fst snd force undefined fail not format read 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 locateme 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 warp as robotnamed robotnumbered knows
 syn keyword Direction east north west south down forward left back right
 syn match Type "\<[A-Z][a-zA-Z_]*\>"

editors/vscode/syntaxes/swarm.tmLanguage.yaml

@@ -46,7 +46,7 @@ repository:
       keyword:
         name: keyword.other
         match: >-
-          \b(self|parent|base|if|inl|inr|case|fst|snd|force|undefined|fail|not|format|chars|split|charat|tochar|key|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|locateme|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|warp|as|robotnamed|robotnumbered|knows)\b
+          \b(self|parent|base|if|inl|inr|case|fst|snd|force|undefined|fail|not|format|read|chars|split|charat|tochar|key|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|locateme|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|warp|as|robotnamed|robotnumbered|knows)\b
       require:
         name: keyword.control.require
         match: \b(require)\b

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

@@ -561,6 +561,7 @@ stepCESK cesk = case cesk of
   In (TInt n) _ s k -> return $ Out (VInt n) s k
   In (TText str) _ s k -> return $ Out (VText str) s k
   In (TBool b) _ s k -> return $ Out (VBool b) s k
+  In (TType ty) _ s k -> return $ Out (VType ty) s k
   -- There should not be any antiquoted variables left at this point.
   In (TAntiText v) _ s k ->
     return $ Up (Fatal (T.append "Antiquoted variable found at runtime: $str:" v)) s k

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

@@ -77,6 +77,7 @@ compareValues v1 = case v1 of
   VSuspend {} -> incomparable v1
   VExc {} -> incomparable v1
   VBlackhole {} -> incomparable v1
+  VType {} -> incomparable v1
 
 -- | Values with different types were compared; this should not be
 --   possible since the type system should catch it.

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

@@ -87,6 +87,7 @@ import Swarm.Game.Universe
 import Swarm.Game.Value
 import Swarm.Language.Capability
 import Swarm.Language.Key (parseKeyComboFull)
+import Swarm.Language.Parser.Value (readValue)
 import Swarm.Language.Pipeline
 import Swarm.Language.Requirements qualified as R
 import Swarm.Language.Syntax
@@ -1208,6 +1209,11 @@ execConst runChildProg c vs s k = do
     Format -> case vs of
       [v] -> return $ mkReturn $ prettyValue v
       _ -> badConst
+    Read -> case vs of
+      [VType ty, VText txt] -> case readValue ty txt of
+        Nothing -> raise Read ["Could not read", showT txt, "at type", prettyText ty]
+        Just v -> return (mkReturn v)
+      _ -> badConst
     Chars -> case vs of
       [VText t] -> return $ mkReturn $ T.length t
       _ -> badConst

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

@@ -38,6 +38,9 @@ pattern VRect x1 y1 x2 y2 = VPair (VPair (VInt x1) (VInt y1)) (VPair (VInt x2) (
 class Valuable a where
   asValue :: a -> Value
 
+instance Valuable Value where
+  asValue = id
+
 instance Valuable Int32 where
   asValue = VInt . fromIntegral
 

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

@@ -1,4 +1,5 @@
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE ViewPatterns #-}
 
 -- |
 -- SPDX-License-Identifier: BSD-3-Clause
@@ -8,6 +9,7 @@ module Swarm.Language.Elaborate where
 
 import Control.Lens (transform, (^.))
 import Swarm.Language.Syntax
+import Swarm.Language.Types
 
 -- | Perform some elaboration / rewriting on a fully type-annotated
 --   term.  This currently performs such operations as rewriting @if@
@@ -23,7 +25,10 @@ elaborate :: TSyntax -> TSyntax
 elaborate = transform rewrite
  where
   rewrite :: TSyntax -> TSyntax
-  rewrite (Syntax' l t cs ty) = Syntax' l (rewriteTerm t) cs ty
+  rewrite = \case
+    syn@(Syntax' l (TConst Read) cs pty@(ptBody -> TyText :->: outTy)) ->
+      Syntax' l (SApp syn (Syntax' NoLoc (TType outTy) mempty (mkTrivPoly TyUnit))) cs pty
+    Syntax' l t cs ty -> Syntax' l (rewriteTerm t) cs ty
 
   rewriteTerm :: TTerm -> TTerm
   rewriteTerm = \case

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

@@ -130,6 +130,7 @@ narrowToPosition s0@(Syntax' _ t _ ty) pos = fromMaybe s0 $ case t of
   TVar {} -> Nothing
   TRequire {} -> Nothing
   TRequireDevice {} -> Nothing
+  TType {} -> Nothing
   -- these should not show up in surface language
   TRef {} -> Nothing
   TRobot {} -> Nothing
@@ -203,6 +204,7 @@ explain trm = case trm ^. sTerm of
   SRcd {} -> literal "A record literal."
   SProj {} -> literal "A record projection."
   STydef {} -> literal "A type synonym definition."
+  TType {} -> literal "A type literal."
   -- type ascription
   SAnnotate lhs typeAnn ->
     Node

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

@@ -16,8 +16,8 @@ import Swarm.Language.Parser.Lex (symbol, tmVar)
 import Swarm.Util (failT, findDup, squote)
 import Text.Megaparsec (sepBy)
 
--- | Parse something using record syntax of the form @{x1 v1, x2 v2,
---   ...}@.  The same parser is used both in parsing record types and
+-- | Parse something using record syntax of the form @x1 v1, x2 v2,
+--   ...@.  The same parser is used both in parsing record types and
 --   record values, so it is factored out into its own module.
 --
 --   The @Parser a@ argument is the parser to use for the RHS of each

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

@@ -0,0 +1,71 @@
+-- |
+-- SPDX-License-Identifier: BSD-3-Clause
+--
+-- Parse values of the Swarm language, indexed by type, by running the
+-- full swarm-lang parser and then checking that the result is a value
+-- of the proper type.
+module Swarm.Language.Parser.Value (readValue) where
+
+import Control.Lens ((^.))
+import Data.Either.Extra (eitherToMaybe)
+import Data.Text (Text)
+import Swarm.Language.Context qualified as Ctx
+import Swarm.Language.Key (parseKeyComboFull)
+import Swarm.Language.Parser (readNonemptyTerm)
+import Swarm.Language.Syntax
+import Swarm.Language.Typecheck (checkTop)
+import Swarm.Language.Types (Type)
+import Swarm.Language.Value
+import Text.Megaparsec qualified as MP
+
+readValue :: Type -> Text -> Maybe Value
+readValue ty txt = do
+  s <- eitherToMaybe $ readNonemptyTerm txt
+  _ <- eitherToMaybe $ checkTop Ctx.empty Ctx.empty Ctx.empty s ty
+  toValue $ s ^. sTerm
+
+toValue :: Term -> Maybe Value
+toValue = \case
+  TUnit -> Just VUnit
+  TDir d -> Just $ VDir d
+  TInt n -> Just $ VInt n
+  TText t -> Just $ VText t
+  TBool b -> Just $ VBool b
+  TApp (TConst c) t2 -> case c of
+    Neg -> toValue t2 >>= negateInt
+    Inl -> VInj False <$> toValue t2
+    Inr -> VInj True <$> toValue t2
+    Key -> do
+      VText k <- toValue t2
+      VKey <$> eitherToMaybe (MP.runParser parseKeyComboFull "" k)
+    _ -> Nothing
+  TPair t1 t2 -> VPair <$> toValue t1 <*> toValue t2
+  TRcd m -> VRcd <$> traverse (>>= toValue) m
+  -- List the other cases explicitly, instead of a catch-all, so that
+  -- we will get a warning if we ever add new constructors in the
+  -- future
+  TConst {} -> Nothing
+  TAntiInt {} -> Nothing
+  TAntiText {} -> Nothing
+  TRequireDevice {} -> Nothing
+  TRequire {} -> Nothing
+  TRequirements {} -> Nothing
+  TVar {} -> Nothing
+  TLam {} -> Nothing
+  TApp {} -> Nothing
+  TLet {} -> Nothing
+  TTydef {} -> Nothing
+  TBind {} -> Nothing
+  TDelay {} -> Nothing
+  TProj {} -> Nothing
+  TAnnotate {} -> Nothing
+  TSuspend {} -> Nothing
+
+-- TODO(#2232): in order to get `read` to work for delay, function,
+-- and/or command types, we will need to handle a few more of the
+-- above cases, e.g. TConst, TLam, TApp, TLet, TBind, TDelay.
+
+negateInt :: Value -> Maybe Value
+negateInt = \case
+  VInt n -> Just (VInt (-n))
+  _ -> Nothing

src/swarm-lang/Swarm/Language/Syntax/AST.hs

@@ -142,6 +142,8 @@ data Term' ty
   | -- | Run the given command, then suspend and wait for a new REPL
     --   input.
     SSuspend (Syntax' ty)
+  | -- | A type literal.
+    TType Type
   deriving
     ( Eq
     , Show

src/swarm-lang/Swarm/Language/Syntax/Constants.hs

@@ -271,6 +271,8 @@ data Const
 
     -- | Turn an arbitrary value into a string
     Format
+  | -- | Try to turn a string into a value
+    Read
   | -- | Concatenate string values
     Concat
   | -- | Count number of characters.
@@ -813,6 +815,7 @@ constInfo c = case c of
   Leq -> binaryOp "<=" 4 N $ shortDoc Set.empty "Check that the left value is lesser or equal to the right one."
   Geq -> binaryOp ">=" 4 N $ shortDoc Set.empty "Check that the left value is greater or equal to the right one."
   Format -> function 1 $ shortDoc Set.empty "Turn an arbitrary value into a string."
+  Read -> function 2 $ shortDoc Set.empty "Try to read a string into a value of the expected type."
   Concat -> binaryOp "++" 6 R $ shortDoc Set.empty "Concatenate the given strings."
   Chars -> function 1 $ shortDoc Set.empty "Counts the number of characters in the text."
   Split ->

src/swarm-lang/Swarm/Language/Syntax/Pretty.hs

@@ -136,6 +136,7 @@ instance PrettyPrec (Term' ty) where
     SSuspend t ->
       pparens (p > 10) $
         "suspend" <+> prettyPrec 11 t
+    TType ty -> prettyPrec p ty
 
 prettyDefinition :: Doc ann -> Var -> Maybe (Poly q Type) -> Syntax' ty -> Doc ann
 prettyDefinition defName x mty t1 =

src/swarm-lang/Swarm/Language/Syntax/Util.hs

@@ -145,6 +145,7 @@ freeVarsS f = go S.empty
     SProj s1 x -> rewrap $ SProj <$> go bound s1 <*> pure x
     SAnnotate s1 pty -> rewrap $ SAnnotate <$> go bound s1 <*> pure pty
     SSuspend s1 -> rewrap $ SSuspend <$> go bound s1
+    TType {} -> pure s
    where
     rewrap s' = Syntax' l <$> s' <*> pure ty <*> pure cmts
 

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

@@ -39,6 +39,7 @@ module Swarm.Language.Typecheck (
 
   -- * Type inference
   inferTop,
+  checkTop,
   infer,
   inferConst,
   check,
@@ -811,6 +812,10 @@ decomposeProdTy = decomposeTyConApp2 TCProd
 inferTop :: TCtx -> ReqCtx -> TDCtx -> Syntax -> Either ContextualTypeErr TSyntax
 inferTop ctx reqCtx tdCtx = runTC ctx reqCtx tdCtx Ctx.empty . infer
 
+-- | Top level type checking function.
+checkTop :: TCtx -> ReqCtx -> TDCtx -> Syntax -> Type -> Either ContextualTypeErr TSyntax
+checkTop ctx reqCtx tdCtx t ty = runTC ctx reqCtx tdCtx Ctx.empty $ check t (toU ty)
+
 -- | Infer the type of a term, returning a type-annotated term.
 --
 --   The only cases explicitly handled in 'infer' are those where
@@ -1094,6 +1099,7 @@ inferConst c = run . runReader @TVCtx Ctx.empty . quantify $ case c of
   Div -> arithBinT
   Exp -> arithBinT
   Format -> [tyQ| a -> Text |]
+  Read -> [tyQ| Text -> a |]
   Concat -> [tyQ| Text -> Text -> Text |]
   Chars -> [tyQ| Text -> Int |]
   Split -> [tyQ| Int -> Text -> (Text * Text) |]
@@ -1387,6 +1393,7 @@ analyzeAtomic locals (Syntax l t) = case t of
   TRequire {} -> return 0
   SRequirements {} -> return 0
   STydef {} -> return 0
+  TType {} -> return 0
   -- Constants.
   TConst c
     -- Nested 'atomic' is not allowed.

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

@@ -112,6 +112,7 @@ module Swarm.Language.Types (
   tydefArity,
   substTydef,
   expandTydef,
+  expandTydefs,
   elimTydef,
   TDCtx,
 
@@ -125,10 +126,11 @@ module Swarm.Language.Types (
 import Control.Algebra (Has, run)
 import Control.Carrier.Reader (runReader)
 import Control.Effect.Reader (Reader, ask)
-import Control.Lens (makeLenses, view)
+import Control.Lens (Plated (..), makeLenses, rewriteM, view)
 import Control.Monad.Free
 import Data.Aeson (FromJSON (..), FromJSON1 (..), ToJSON (..), ToJSON1 (..), genericLiftParseJSON, genericLiftToJSON, genericParseJSON, genericToJSON)
 import Data.Data (Data)
+import Data.Data.Lens (uniplate)
 import Data.Eq.Deriving (deriveEq1)
 import Data.Fix
 import Data.Foldable (fold)
@@ -299,6 +301,9 @@ instance FromJSON1 TypeF where
 --   with 'Type' as if it were defined in a directly recursive way.
 type Type = Fix TypeF
 
+instance Plated Type where
+  plate = uniplate
+
 newtype IntVar = IntVar Int
   deriving (Show, Data, Eq, Ord, Generic, Hashable)
 
@@ -818,6 +823,16 @@ expandTydef userTyCon tys = do
       tydefInfo = fromMaybe (error errMsg) mtydefInfo
   return $ substTydef tydefInfo tys
 
+-- | Expand *all* applications of user-defined type constructors
+--   everywhere in a type.
+expandTydefs :: forall sig m. (Has (Reader TDCtx) sig m) => Type -> m Type
+expandTydefs = rewriteM expand
+ where
+  expand :: Type -> m (Maybe Type)
+  expand = \case
+    TyUser u tys -> Just <$> expandTydef u tys
+    _ -> pure Nothing
+
 -- | Given the definition of a type alias, substitute the given
 --   arguments into its body and return the resulting type.
 substTydef :: forall t. Typical t => TydefInfo -> [t] -> t

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

@@ -44,7 +44,7 @@ import Swarm.Language.Requirements.Type (ReqCtx, Requirements)
 import Swarm.Language.Syntax
 import Swarm.Language.Syntax.Direction
 import Swarm.Language.Typed
-import Swarm.Language.Types (Polytype, TCtx, TDCtx, TydefInfo)
+import Swarm.Language.Types (Polytype, TCtx, TDCtx, TydefInfo, Type)
 import Swarm.Pretty (prettyText)
 
 -- | A /value/ is a term that cannot (or does not) take any more
@@ -119,6 +119,9 @@ data Value where
   --   <http://www.lel.ed.ac.uk/~gpullum/loopsnoop.html cannot detect
   --   /all/ infinite loops this way>.)
   VBlackhole :: Value
+  -- | A special value used to represent runtime type information
+  --   passed to ad-hoc polymorphic functions.
+  VType :: Type -> Value
   deriving (Eq, Show, Generic, Hashable)
 
 -- | A value context is a mapping from variable names to their runtime
@@ -241,3 +244,4 @@ valueToTerm = \case
   VSuspend t _ -> TSuspend t
   VExc -> TConst Undefined
   VBlackhole -> TConst Undefined
+  VType _ -> TConst Undefined

swarm.cabal

@@ -460,6 +460,7 @@ library swarm-lang
     Swarm.Language.Parser.Term
     Swarm.Language.Parser.Type
     Swarm.Language.Parser.Util
+    Swarm.Language.Parser.Value
     Swarm.Language.Pipeline
     Swarm.Language.Pipeline.QQ
     Swarm.Language.Requirements