Suggestions from code review

This commit is contained in:
craigmc08 2021-07-30 16:53:51 -04:00 committed by Craig McIlwrath
parent d335562263
commit 6f178115dc
6 changed files with 50 additions and 9 deletions

View File

@ -134,6 +134,16 @@ type system. Some special conventions are followed:
\Gamma \vdash \texttt{[ } e_1 \texttt{,} \ldots \texttt{,} e_n \texttt{ ]} : [\tau]
}
\inferrule[EmptyList]{ }{
\Gamma \vdash \texttt{[]} : emptyList
}
\inferrule[AnyList]{
\Gamma \vdash e : emptyList
}{
\Gamma \vdash e : [\tau], \forall \tau
}
\inferrule[Dot]{
\Gamma \vdash e : \{ \texttt{k}: \tau, \ldots \}
}{
@ -160,6 +170,13 @@ type system. Some special conventions are followed:
An ambiguity that arises is whether \texttt{x = [\{a: 1\}, \{\}]} is well-typed,
and if \texttt{x}'s type is $[\{\}]$ or $[\{ a: number? \}]$.
The rules \textsc{EmptyList} and \textsc{AnyList} are one way of allowing empty
lists to type check, since \textsc{List} does not allow picking a type for an
empty list. An alternative would be allowing type variables to be given to any
ambiguous expressions, like an empty list, and having a separate pass to resolve
the ambiguities from surrounding context. The current method for checking empty
lists was chosen as it gives a much simpler implementation.
\subsubsection{Type Checking}
There are two phases to the type checker:

View File

@ -13,6 +13,11 @@ data Type
| EnumType String
| DictType (H.HashMap String DictEntryType)
| ListType Type
| -- | A temporary type given to an empty list. All occurences of this type
-- will have been changed to an appropriate "ListType" when "typeCheck" is
-- finished. See section 2.2 of the wasplang document for more information
-- on this.
EmptyListType
| StringType
| NumberType
| BoolType

View File

@ -95,7 +95,8 @@ inferExprType (P.Quoter tag _) = throw $ QuoterUnknownTag tag
inferExprType (P.List values) = do
typedValues <- mapM inferExprType values
case unify <$> nonEmpty typedValues of
Nothing -> throw EmptyListNotImplemented
-- Apply [EmptyList]
Nothing -> return $ List [] EmptyListType
Just (Left e) ->
throw e
Just (Right (unifiedValues, unifiedType)) ->
@ -151,7 +152,10 @@ unify exprs = do
unifyTypes :: Type -> Type -> Either TypeError Type
unifyTypes type1 type2
| type1 == type2 = Right type1
-- Two lists unify only if their inner types unify
-- Apply [AnyList]: an empty list can unify with any other list
unifyTypes EmptyListType typ@(ListType _) = Right typ
unifyTypes typ@(ListType _) EmptyListType = Right typ
-- Two non-empty lists unify only if their inner types unify
unifyTypes type1@(ListType elemType1) type2@(ListType elemType2) =
annotateError $ ListType <$> unifyTypes elemType1 elemType2
where
@ -198,7 +202,9 @@ unifyTypes type1 type2 = Left $ UnificationError ReasonUncoercable type1 type2
weaken :: Type -> TypedExpr -> Either TypeError TypedExpr
weaken type' expr
| exprType expr == type' = Right expr
-- A list can be weakened to @typ@ if
-- Apply [AnyList]: An empty list can be weakened to any list type
weaken type'@(ListType _) (List [] EmptyListType) = return $ List [] type'
-- A non-empty list can be weakened to @typ@ if
-- - @typ@ is of the form @ListType type'@
-- - Every value in the list can be weakened to @type'@
weaken type'@(ListType elemType') expr@(List elems _) = do

View File

@ -29,8 +29,6 @@ data TypeError
| UndefinedIdentifier String
| QuoterUnknownTag String
| DictDuplicateField String
| -- | TODO: Temporary "solution" to missing type inference for empty lists
EmptyListNotImplemented
deriving (Eq, Show)
-- | Describes a reason that a @UnificationError@ or @WeakenError@ happened

View File

@ -72,6 +72,12 @@ spec_Internal = do
let a = Dict [] (DictType H.empty)
let b = Dict [("a", BoolLiteral True)] $ DictType $ H.singleton "a" $ DictRequired BoolType
unify (a :| [b]) `shouldBe` (unify (a :| [b]) >>= unify . fst)
it "Unifies an empty list with any other list" $ do
let a = List [] EmptyListType
let b = List [StringLiteral "a"] (ListType StringType)
let expected = ListType StringType
fmap (fmap exprType . fst) (unify (a :| [b]))
`shouldBe` Right (expected :| [expected])
describe "inferExprType" $ do
testSuccess "Types string literals as StringType" (P.StringLiteral "string") StringType
@ -110,11 +116,10 @@ spec_Internal = do
(P.Dict [("a", P.IntegerLiteral 5), ("a", P.IntegerLiteral 6)])
(DictDuplicateField "a")
-- TODO: this test must be removed/changed when empty lists are implemented.
testFail
"Fails to type check an empty list"
testSuccess
"Type checks an empty list as EmptyListType"
(P.List [])
EmptyListNotImplemented
EmptyListType
testSuccess
"Type checks a list where all elements have the same type"
(P.List [P.IntegerLiteral 5, P.DoubleLiteral 1.6])

View File

@ -69,3 +69,13 @@ spec_TypeChecker = do
let actual = typeCheck typeDefs ast
let expected = Right $ TypedAST [Decl "Cucumber" (Var "Dill" (EnumType "flavor")) (DeclType "food")]
actual `shouldBe` expected
it "Type checks an empty list in a declaration" $ do
let ast = P.AST [P.Decl "rooms" "Bedrooms" (P.List [])]
let typeDefs =
TD.TypeDefinitions
{ TD.declTypes = H.singleton "rooms" (TD.DeclType "rooms" $ ListType StringType),
TD.enumTypes = H.empty
}
let actual = typeCheck typeDefs ast
let expected = Right $ TypedAST [Decl "Bedrooms" (List [] (ListType StringType)) (DeclType "rooms")]
actual `shouldBe` expected