Add void type (#735)

Closes #665 

### todo
- [x] add void to the parser for types
- [x] add two tests
- [ ] mention `void` in the description of an `ADT calculator`

src/Swarm/Language/Parse.hs

@@ -81,7 +81,8 @@ reservedWords :: [Text]
 reservedWords =
   map (syntax . constInfo) (filter isUserFunc allConst)
     ++ map (dirSyntax . dirInfo) allDirs
-    ++ [ "unit"
+    ++ [ "void"
+       , "unit"
        , "int"
        , "text"
        , "dir"
@@ -204,7 +205,8 @@ parseType = makeExprParser parseTypeAtom table
 
 parseTypeAtom :: Parser Type
 parseTypeAtom =
-  TyUnit <$ reserved "unit"
+  TyVoid <$ reserved "void"
+    <|> TyUnit <$ reserved "unit"
     <|> TyVar <$> identifier
     <|> TyInt <$ reserved "int"
     <|> TyText <$ reserved "text"

src/Swarm/Language/Pretty.hs

@@ -55,6 +55,7 @@ pparens True = parens
 pparens False = id
 
 instance PrettyPrec BaseTy where
+  prettyPrec _ BVoid = "void"
   prettyPrec _ BUnit = "unit"
   prettyPrec _ BInt = "int"
   prettyPrec _ BDir = "dir"

src/Swarm/Language/Typecheck.hs

@@ -42,6 +42,7 @@ module Swarm.Language.Typecheck (
   check,
   decomposeCmdTy,
   decomposeFunTy,
+  isSimpleUType,
 ) where
 
 import Control.Category ((>>>))

src/Swarm/Language/Types.hs

@@ -23,6 +23,7 @@ module Swarm.Language.Types (
   tyVars,
   pattern TyBase,
   pattern TyVar,
+  pattern TyVoid,
   pattern TyUnit,
   pattern TyInt,
   pattern TyText,
@@ -39,6 +40,7 @@ module Swarm.Language.Types (
   UType,
   pattern UTyBase,
   pattern UTyVar,
+  pattern UTyVoid,
   pattern UTyUnit,
   pattern UTyInt,
   pattern UTyText,
@@ -97,7 +99,9 @@ import Witch
 
 -- | Base types.
 data BaseTy
-  = -- | The unit type, with a single inhabitant.
+  = -- | The void type, with no inhabintants.
+    BVoid
+  | -- | The unit type, with a single inhabitant.
     BUnit
   | -- | Signed, arbitrary-size integers.
     BInt
@@ -290,6 +294,9 @@ pattern TyBase b = Fix (TyBaseF b)
 pattern TyVar :: Var -> Type
 pattern TyVar v = Fix (TyVarF v)
 
+pattern TyVoid :: Type
+pattern TyVoid = Fix (TyBaseF BVoid)
+
 pattern TyUnit :: Type
 pattern TyUnit = Fix (TyBaseF BUnit)
 
@@ -335,6 +342,9 @@ pattern UTyBase b = UTerm (TyBaseF b)
 pattern UTyVar :: Var -> UType
 pattern UTyVar v = UTerm (TyVarF v)
 
+pattern UTyVoid :: UType
+pattern UTyVoid = UTerm (TyBaseF BVoid)
+
 pattern UTyUnit :: UType
 pattern UTyUnit = UTerm (TyBaseF BUnit)
 

test/unit/TestLanguagePipeline.hs

@@ -10,6 +10,8 @@ import Data.Text (Text)
 import Data.Text qualified as T
 import Data.Text.Encoding qualified as T
 import Swarm.Language.Pipeline (processTerm)
+import Swarm.Language.Typecheck (isSimpleUType)
+import Swarm.Language.Types
 import Test.Tasty
 import Test.Tasty.HUnit
 import Witch (from)
@@ -233,6 +235,16 @@ testLanguagePipeline =
             "invalid hex literal"
             (process "0xabcD6G2" "1:8:\n  |\n1 | 0xabcD6G2\n  |        ^\nunexpected 'G'\n")
         ]
+    , testGroup
+        "void type"
+        [ testCase
+            "void - isSimpleUType"
+            ( assertBool "" $ isSimpleUType UTyVoid
+            )
+        , testCase
+            "void - valid type signature"
+            (valid "def f : void -> a = \\x. undefined end")
+        ]
     ]
  where
   valid = flip process ""

test/unit/TestPretty.hs

@@ -5,6 +5,7 @@ module TestPretty where
 
 import Swarm.Language.Pretty
 import Swarm.Language.Syntax hiding (mkOp)
+import Swarm.Language.Types
 import Test.Tasty
 import Test.Tasty.HUnit
 
@@ -77,6 +78,10 @@ testPrettyConst =
         ( equalPretty "(1, 2, 3)" $
             TPair (TInt 1) (TPair (TInt 2) (TInt 3))
         )
+    , testCase
+        "void type"
+        ( assertEqual "" "void" . show $ ppr TyVoid
+        )
     ]
  where
   equalPretty :: String -> Term -> Assertion