require explicit forall on polymorphic types

data/entities.yaml

@@ -377,7 +377,7 @@
   - |
     An equipped `linotype`{=entity} device enables the `format` command:
     ```
-    format : a -> text
+    format : ∀ a. a -> text
     ```
     which can turn any value into a suitable text representation.
   properties: [portable]
@@ -440,7 +440,7 @@
     An equipped `string`{=entity} device enables several commands for working with
     `text`{=type} values:
   - |
-    `format : a -> text` can turn any value into a suitable text
+    `format : ∀ a. a -> text` can turn any value into a suitable text
     representation.
   - |
     The infix operator `++ : text -> text -> text`{=snippet}
@@ -1202,18 +1202,18 @@
     `void`{=type} that correspond to 1 and 0, respectively.
   - |
     The product of two types is a type of pairs, since, for example,
-    if `t`{=type} is a type with three elements, then there are 2 * 3 = 6
-    different pairs containing a `bool`{=type} and a `t`{=type}, that is, 6 elements
-    of type `bool * t`{=type}.  For working with products of types, the ADT
+    if `t`{=snippet} is a type with three elements, then there are 2 * 3 = 6
+    different pairs containing a `bool`{=type} and a `t`{=snippet}, that is, 6 elements
+    of type `bool * t`{=snippet}.  For working with products of types, the ADT
     calculator enables pair syntax `(1, "Hi!")` as well as the projection
-    functions `fst : a * b -> a` and `snd : a * b -> b`.
+    functions `fst : ∀ a b. a * b -> a` and `snd : ∀ a b. a * b -> b`.
   - |
     The sum of two types is a type with two options; for example, a
-    value of type `bool + t`{=type} is either a `bool`{=type} value or a `t`{=type} value,
+    value of type `bool + t`{=snippet} is either a `bool`{=type} value or a `t`{=snippet} value,
     and there are `2 + 3 == 5` such values.  For working with sums of
     types, the ADT calculator provides the injection functions `inl :
-    a -> a + b` and `inr : b -> a + b`, as well as the case analysis
-    function `case : (a + b) -> (a -> c) -> (b -> c) -> c`.  For
+    ∀ a b. a -> a + b` and `inr : ∀ a b. b -> a + b`, as well as the case analysis
+    function `case : ∀ a b c. (a + b) -> (a -> c) -> (b -> c) -> c`.  For
     example, `case (inl 3) (\x. 2*x) (\y. 3*y) == 6`, and `case (inr
     3) (\x. 2*x) (\y. 3*y) == 9`.
 
@@ -1353,9 +1353,9 @@
     It returns a reference to the nearest actor, or a unit value if
     none are found.
   - |
-    `meetAll : (b -> actor -> cmd b) -> b -> cmd b` runs a command on
+    `meetAll : ∀ b. (b -> actor -> cmd b) -> b -> cmd b` runs a command on
     every nearby actor (other than oneself), folding over the results
-    to compute a final result of type `b`{=type}.  For example, if
+    to compute a final result of type `b`{=snippet}.  For example, if
     `x`{=snippet}, `y`{=snippet}, and `z`{=snippet}
     are nearby actors, then `meetAll f b0`{=snippet} is equivalent to
     `b1 <- f b0 x; b2 <- f b1 y; f b2 z`{=snippet}.

data/scenarios/Tutorials/conditionals.yaml

@@ -25,28 +25,28 @@ objectives:
         it is simply a built-in function of type
       - |
         ```
-        if : bool -> {a} -> {a} -> a
+        if : ∀ a. bool -> {a} -> {a} -> a
         ```
       - |
         It takes a boolean expression and then returns either the first or second subsequent
         argument, depending on whether the boolean expression is true or false, respectively.
       - |
-        The type variable `a`{=type} can stand for any type; `{a}`{=type}
-        indicates a *delayed* expression of type `a`{=type}.  Normally,
+        The type variable `a`{=snippet} can stand for any type; `{a}`{=snippet}
+        indicates a *delayed* expression of type `a`{=snippet}.  Normally,
         function arguments are evaluated strictly before the function
         is called. Delayed expressions, on the other hand, are not
         evaluated until needed.  In this case, we want to make sure
         that only the correct branch is evaluated.  To write a value
         of type, say, `{int}`{=type}, we just surround a value of type `int`{=type}
         in curly braces, like `{3}`.  This is why arguments to `build`
         must also be in curly braces: the type of `build`
-        is `{cmd a} -> cmd robot`{=type}.
+        is `∀ a. {cmd a} -> cmd robot`{=type}.
       - |
         **TIP:** Note that `if` requires a `bool`{=type}, not a `cmd bool`{=type}!  So you cannot directly say
         `if (ishere "very small rock") {...} {...}`{=snippet}.
         Instead you can write `b <- ishere "very small rock"; if b {...} {...}`{=snippet}.
         You might enjoy writing your own function of
-        type `cmd bool -> {cmd a} -> {cmd a} -> cmd a`{=type} to encapsulate this pattern.
+        type `∀ a. cmd bool -> {cmd a} -> {cmd a} -> cmd a`{=type} to encapsulate this pattern.
       - |
         **TIP:** the two branches of an `if` must have the same type. In particular,
         `if ... {grab} {}`{=snippet} is not

data/scenarios/Tutorials/farming.sw

@@ -5,10 +5,10 @@ def tR = turn right end;
 def tL = turn left end;
 def tB = turn back end;
 def forever = \c. c ; forever c end;
-def ifC : cmd bool -> {cmd a} -> {cmd a} -> cmd a = \test. \then. \else.
+def ifC : ∀ a. cmd bool -> {cmd a} -> {cmd a} -> cmd a = \test. \then. \else.
   b <- test; if b then else
 end;
-def while : cmd bool -> {cmd a} -> cmd unit = \test. \body.
+def while : ∀ a. cmd bool -> {cmd a} -> cmd unit = \test. \body.
   ifC test {force body ; while test body} {}
 end;
 def giveall : actor -> text -> cmd unit = \r. \thing.

editors/emacs/swarm-mode.el

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

editors/vim/swarm.vim

@@ -1,4 +1,4 @@
-syn keyword Keyword def end let in require
+syn keyword Keyword def end let in require forall
 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 path push stride turn grab harvest 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 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/list.sw

@@ -179,7 +179,7 @@ def index = \i.\xs.
     {index (i-1) (tail xs)}
 end
 
-def for : int -> int -> (int -> cmd a) -> cmd unit = \s.\e.\act.
+def for : forall a. int -> int -> (int -> cmd a) -> cmd unit = \s.\e.\act.
   if (s == e) {}
   {act s; for (s+1) e act}
 end

example/multi-key-handler.sw

@@ -1,11 +1,11 @@
 // Proof of concept illustrating the possibility of key
 // handlers that process multi-key sequences.
 
-def cons : a * b -> (a -> b) -> (a -> b) = \p. \k. \a.
+def cons : forall a b. a * b -> (a -> b) -> (a -> b) = \p. \k. \a.
   if (a == fst p) {snd p} {k a}
 end
 
-def nil : a -> cmd unit = \a. return () end
+def nil : forall a. a -> cmd unit = \a. return () end
 
 // The delay around the first argument is necessary to prevent
 // infinite recursion

example/pilotmode.sw

@@ -1,8 +1,8 @@
-def cons : a * b -> (a -> b) -> (a -> b) = \p. \k. \a.
+def cons : forall a b. a * b -> (a -> b) -> (a -> b) = \p. \k. \a.
   if (a == fst p) {snd p} {k a}
 end
 
-def nil : a -> cmd unit = \a. return () end
+def nil : forall a. a -> cmd unit = \a. return () end
 
 // Suitable to use as e.g.
 //   installKeyHandler "(S-)←↓↑→ [Del] [g]rab [h]arvest [d]rill [s]can [b]locked [u]pload" pilot

src/Swarm/Language/Parse.hs

@@ -104,6 +104,7 @@ reservedWords =
        , "true"
        , "false"
        , "forall"
+       , "∀"
        , "require"
        , "requirements"
        ]
@@ -181,27 +182,31 @@ brackets = between (symbol "[") (symbol "]")
 -- Parser
 
 -- | Parse a Swarm language polytype, which starts with an optional
---   quanitifation (@forall@ followed by one or more variables and a
+--   quanitifation (@forall@ or @∀@ followed by one or more variables and a
 --   period) followed by a type.  Note that anything accepted by
 --   'parseType' is also accepted by 'parsePolytype'.
+--
+--   @parsePolytype@ does /not/ allow implicit quantification: any
+--   type variables must be explicitly introduced by a @forall@.
 parsePolytype :: Parser Polytype
 parsePolytype =
-  join $
-    quantify
-      <$> (fromMaybe [] <$> optional (reserved "forall" *> some identifier <* symbol "."))
-      <*> parseType
+  join
+    $ quantify
+    <$> (fromMaybe [] <$> optional (quantifier *> some identifier <* symbol "."))
+    <*> parseType
  where
+  quantifier = reserved "forall" <|> reserved "∀"
+
   quantify :: [Var] -> Type -> Parser Polytype
   quantify xs ty
-    -- Iplicitly quantify over free type variables if the user didn't write a forall
-    | null xs = return $ Forall (S.toList free) ty
-    -- Otherwise, require all variables to be explicitly quantified
+    -- Wrap in a Forall quantifier as long as there are no free type variables.
     | S.null free = return $ Forall xs ty
     | otherwise =
-        fail $
-          unlines
+        fail
+          $ unlines
             [ "  Type contains free variable(s): " ++ unwords (map from (S.toList free))
-            , "  Try adding them to the 'forall'."
+            , "  - If you don't want a polymorphic type, maybe check your spelling."
+            , "  - If you do want a polymorphic type, you must explicitly bind all type variables with a 'forall'."
             ]
    where
     free = tyVars ty `S.difference` S.fromList xs

src/Swarm/Language/Typecheck.hs

@@ -742,7 +742,7 @@ inferConst c = case c of
   Selfdestruct -> [tyQ| cmd unit |]
   Move -> [tyQ| cmd unit |]
   Backup -> [tyQ| cmd unit |]
-  Path -> [tyQ| (unit + int) -> ((int * int) + entity) -> cmd (unit + dir) |]
+  Path -> [tyQ| (unit + int) -> ((int * int) + text) -> cmd (unit + dir) |]
   Push -> [tyQ| cmd unit |]
   Stride -> [tyQ| int -> cmd unit |]
   Turn -> [tyQ| dir -> cmd unit |]
@@ -758,8 +758,8 @@ inferConst c = case c of
   Has -> [tyQ| text -> cmd bool |]
   Equipped -> [tyQ| text -> cmd bool |]
   Count -> [tyQ| text -> cmd int |]
-  Reprogram -> [tyQ| actor -> {cmd a} -> cmd unit |]
-  Build -> [tyQ| {cmd a} -> cmd actor |]
+  Reprogram -> [tyQ| ∀ a. actor -> {cmd a} -> cmd unit |]
+  Build -> [tyQ| ∀ a. {cmd a} -> cmd actor |]
   Drill -> [tyQ| dir -> cmd (unit + text) |]
   Use -> [tyQ| text -> dir -> cmd (unit + text) |]
   Salvage -> [tyQ| cmd unit |]
@@ -791,22 +791,22 @@ inferConst c = case c of
   Parent -> [tyQ| actor |]
   Base -> [tyQ| actor |]
   Meet -> [tyQ| cmd (unit + actor) |]
-  MeetAll -> [tyQ| (b -> actor -> cmd b) -> b -> cmd b |]
+  MeetAll -> [tyQ| ∀ b. (b -> actor -> cmd b) -> b -> cmd b |]
   Whoami -> [tyQ| cmd text |]
   Setname -> [tyQ| text -> cmd unit |]
   Random -> [tyQ| int -> cmd int |]
   Run -> [tyQ| text -> cmd unit |]
-  If -> [tyQ| bool -> {a} -> {a} -> a |]
-  Inl -> [tyQ| a -> a + b |]
-  Inr -> [tyQ| b -> a + b |]
-  Case -> [tyQ|a + b -> (a -> c) -> (b -> c) -> c |]
-  Fst -> [tyQ| a * b -> a |]
-  Snd -> [tyQ| a * b -> b |]
-  Force -> [tyQ| {a} -> a |]
-  Return -> [tyQ| a -> cmd a |]
-  Try -> [tyQ| {cmd a} -> {cmd a} -> cmd a |]
-  Undefined -> [tyQ| a |]
-  Fail -> [tyQ| text -> a |]
+  If -> [tyQ| ∀ a. bool -> {a} -> {a} -> a |]
+  Inl -> [tyQ| ∀ a b. a -> a + b |]
+  Inr -> [tyQ| ∀ a b. b -> a + b |]
+  Case -> [tyQ| ∀ a b c. a + b -> (a -> c) -> (b -> c) -> c |]
+  Fst -> [tyQ| ∀ a b. a * b -> a |]
+  Snd -> [tyQ| ∀ a b. a * b -> b |]
+  Force -> [tyQ| ∀ a. {a} -> a |]
+  Return -> [tyQ| ∀ a. a -> cmd a |]
+  Try -> [tyQ| ∀ a. {cmd a} -> {cmd a} -> cmd a |]
+  Undefined -> [tyQ| ∀ a. a |]
+  Fail -> [tyQ| ∀ a. text -> a |]
   Not -> [tyQ| bool -> bool |]
   Neg -> [tyQ| int -> int |]
   Eq -> cmpBinT
@@ -822,25 +822,25 @@ inferConst c = case c of
   Mul -> arithBinT
   Div -> arithBinT
   Exp -> arithBinT
-  Format -> [tyQ| a -> text |]
+  Format -> [tyQ| ∀ a. a -> text |]
   Concat -> [tyQ| text -> text -> text |]
   Chars -> [tyQ| text -> int |]
   Split -> [tyQ| int -> text -> (text * text) |]
   CharAt -> [tyQ| int -> text -> int |]
   ToChar -> [tyQ| int -> text |]
-  AppF -> [tyQ| (a -> b) -> a -> b |]
+  AppF -> [tyQ| ∀ a b. (a -> b) -> a -> b |]
   Swap -> [tyQ| text -> cmd text |]
-  Atomic -> [tyQ| cmd a -> cmd a |]
-  Instant -> [tyQ| cmd a -> cmd a |]
+  Atomic -> [tyQ| ∀ a. cmd a -> cmd a |]
+  Instant -> [tyQ| ∀ a. cmd a -> cmd a |]
   Key -> [tyQ| text -> key |]
   InstallKeyHandler -> [tyQ| text -> (key -> cmd unit) -> cmd unit |]
   Teleport -> [tyQ| actor -> (int * int) -> cmd unit |]
-  As -> [tyQ| actor -> {cmd a} -> cmd a |]
+  As -> [tyQ| ∀ a. actor -> {cmd a} -> cmd a |]
   RobotNamed -> [tyQ| text -> cmd actor |]
   RobotNumbered -> [tyQ| int -> cmd actor |]
   Knows -> [tyQ| text -> cmd bool |]
  where
-  cmpBinT = [tyQ| a -> a -> bool |]
+  cmpBinT = [tyQ| ∀ a. a -> a -> bool |]
   arithBinT = [tyQ| int -> int -> int |]
 
 -- | @check t ty@ checks that @t@ has type @ty@, returning a

test/unit/TestLanguagePipeline.hs

@@ -32,12 +32,28 @@ testLanguagePipeline =
   testGroup
     "Language - pipeline"
     [ testCase "end semicolon #79" (valid "def a = 41 end def b = a + 1 end def c = b + 2 end")
-    , testCase
-        "quantification #148 - implicit"
-        (valid "def id : a -> a = \\x. x end; id move")
     , testCase
         "quantification #148 - explicit"
         (valid "def id : forall a. a -> a = \\x. x end; id move")
+    , testCase
+        "quantification #148 - explicit with ∀"
+        (valid "def id : ∀ a. a -> a = \\x. x end; id move")
+    , testCase
+        "quantification #148 - disallow implicit"
+        ( process
+            "def id : a -> a = \\x. x end; id move"
+            ( T.unlines
+                [ "1:17:"
+                , "  |"
+                , "1 | def id : a -> a = \\x. x end; id move"
+                , "  |                 ^"
+                , "  Type contains free variable(s): a"
+                , "  - If you don't want a polymorphic type, maybe check your spelling."
+                , "  - If you do want a polymorphic type, you must explicitly bind all type variables with a 'forall'."
+                , ""
+                ]
+            )
+        )
     , testCase
         "quantification #148 - explicit with free tyvars"
         ( process
@@ -48,7 +64,8 @@ testLanguagePipeline =
                 , "1 | def id : forall a. b -> b = \\x. x end; id move"
                 , "  |                           ^"
                 , "  Type contains free variable(s): b"
-                , "  Try adding them to the 'forall'."
+                , "  - If you don't want a polymorphic type, maybe check your spelling."
+                , "  - If you do want a polymorphic type, you must explicitly bind all type variables with a 'forall'."
                 , ""
                 ]
             )
@@ -254,7 +271,7 @@ testLanguagePipeline =
             )
         , testCase
             "valid type signature"
-            (valid "def f : void -> a = \\x. undefined end")
+            (valid "def f : ∀ a. void -> a = \\x. undefined end")
         ]
     , testGroup
         "record type"
@@ -316,13 +333,13 @@ testLanguagePipeline =
             (process "1 : text" "1:1: Type mismatch:\n  From context, expected `1` to have type `text`,\n  but it actually has type `int`")
         , testCase
             "type ascription with a polytype"
-            (valid "((\\x . x) : a -> a) 3")
+            (valid "((\\x . x) : forall a. a -> a) 3")
         , testCase
             "type ascription too general"
-            (process "1 : a" "1:1: Type mismatch:\n  From context, expected `1` to have type `s0`,\n  but it actually has type `int`")
+            (process "1 : forall a. a" "1:1: Type mismatch:\n  From context, expected `1` to have type `s0`,\n  but it actually has type `int`")
         , testCase
             "type specialization through type ascription"
-            (valid "fst:(int + b) * a -> int + b")
+            (valid "fst: forall a b. (int + b) * a -> int + b")
         , testCase
             "type ascription doesn't allow rank 2 types"
             ( process
@@ -409,8 +426,12 @@ testLanguagePipeline =
     Left e
       | not (T.null expect) && expect `T.isPrefixOf` e -> pure ()
       | otherwise ->
-          error $
-            "Unexpected failure:\n\n  " <> show e <> "\n\nExpected:\n\n  " <> show expect <> "\n"
+          error
+            $ "Unexpected failure:\n\n  "
+            <> show e
+            <> "\n\nExpected:\n\n  "
+            <> show expect
+            <> "\n"
     Right _
       | expect == "" -> pure ()
       | otherwise -> error "Unexpected success"