Improving Type-checking

[balacij]

In our last meeting, @JacquesCarette mentioned that we should give priority to cleaning up things related to the type checker. So, let's discuss and confirm the nature of our work and what kind of changes we can/should make needed to “clean up” the type checker. In other words, let's figure out what “clean up” means 😉 .

Where it's at

Quick recap:

Language	Typed?
Expr	Yes
ModelExpr	No
CodeExpr	No

Design choices

Recalling a few of our design choices:

1. The type-checker does not piggyback on Haskell's type system, building our own type-checker that checks whole expressions. We wanted to permit ill-typed expressions in these languages, in specific scenarios, and we also ended up preferring to stray away from GADT because of two reasons (IIRC):
   1. We were (at the time) reluctant to add a type argument to QuantityDict to carry type information, and,
   2. even if we preferred that, we could not easily do that because limitations of the current ChunkDB design (unblocked by Merging chunk maps into a single map via Data.Typeable #2873).
2. We split our previous monolithic Expr into the 3 flavours so that we can restrict certain terms and features to specific areas of code.
   • Expr is for simpler mathematics, expressions with a definite value.
   • CodeExpr is an extension of Expr with extra features for OO.
   • ModelExpr is an extension of Expr with all the goodies we normally use in pure mathematics and analysis (well, not all, but more than Expr).
3. We opted to go for a bidirectional type-checker design. The current type-checker we have is rather uncomplicated as well, as it only supports Expr.

Unfortunately, we only got to typing Expr, but now we want to extend it to type checking the others, whilst minimizing code duplication, amongst other things.

How the current type-checker works

The current type-checker is built around the below code:

Drasil/code/drasil-lang/lib/Language/Drasil/WellTyped.hs

Lines 10 to 38 in 85cf74d

	-- TODO: Rather than using a flat String, it would be better to a
	-- ``breadcrumb''-style error data type that can provide a traceable path
	-- to issues in an expression. The breadcrumbs could then be formatted
	-- into a flat String, such as it is now, or into alternative AST views
	-- that show exactly where typing went awry.
	type TypeError = String
	-- | We can only type check 'UID's within a type context relating 'UID's to
	-- types since they don't carry any type information.
	type TypingContext t = M.Map UID t
	-- | Look for a known type of a specific 'UID'.
	inferFromContext :: TypingContext t -> UID -> Either t TypeError
	inferFromContext cxt u = maybe
	(Right $ "`" ++ show u ++ "` lacks type binding in context")
	Left
	(M.lookup u cxt)
	-- | Build a bidirectional type checker for your expression language, e, with
	-- respect to a specific type universe, t.
	class (Eq t, Show t) => Typed e t where
	-- | Given a typing context and an expression, infer a unique type or explain
	-- what went awry.
	infer :: TypingContext t -> e -> Either t TypeError
	-- | Given a typing context, an expression, and an expected type, check if the
	-- expression can satisfy the expectation.
	check :: TypingContext t -> e -> t -> Either t TypeError

In the above code, we see:

1. A “type error” type (a String), which is currently used (attempted) to build a tree view of expressions for when type-checking fails, so that we can print out meaningful error messages about where issues occurred, at the AST level.
2. A “typing context” type (a Map of UIDs to types), which is used to provide the environment of available variables to the type-checker, and for the type-checker to manipulate (~semi-writable -- overwrites only permitted for appended types) as needed.
3. A “typed” typeclass, which is used to indicate that some_thing_ can be typed against a specific type system/language.

Recalling the code related to Expr, we have a type-checker that relies purely on simple inference:

Drasil/code/drasil-lang/lib/Language/Drasil/Expr/Lang.hs

Lines 232 to 428 in 85cf74d

	instance Typed Expr Space where
	check :: TypingContext Space -> Expr -> Space -> Either Space TypeError
	check = typeCheckByInfer
	infer :: TypingContext Space -> Expr -> Either Space TypeError
	infer cxt (Lit lit) = infer cxt lit
	infer cxt (AssocA op exs) = allOfType cxt exs sp sp
	$ "Associative arithmetic operation expects all operands to be of the same expected type (" ++ show sp ++ ")."
	where
	sp = assocArithOperToTy op
	infer cxt (AssocB _ exs) = allOfType cxt exs S.Boolean S.Boolean
	$ "Associative boolean operation expects all operands to be of the same type (" ++ show S.Boolean ++ ")."
	infer cxt (C uid) = inferFromContext cxt uid
	infer cxt (FCall uid exs) = case (inferFromContext cxt uid, map (infer cxt) exs) of
	(Left (S.Function params out), exst) -> if NE.toList params == lefts exst
	then Left out
	else Right $ "Function `" ++ show uid ++ "` expects parameters of types: " ++ show params ++ ", but received: " ++ show (lefts exst) ++ "."
	(Left s, _) -> Right $ "Function application on non-function `" ++ show uid ++ "` (" ++ show s ++ ")."
	(Right x, _) -> Right x
	infer cxt (Case _ ers)
	| null ers = Right "Case contains no expressions, no type to infer."
	| all (\(ne, _) -> infer cxt ne == eT) (tail ers) = eT
	| otherwise = Right "Expressions in case statement contain different types."
	where
	(fe, _) = head ers
	eT = infer cxt fe
	infer cxt (Matrix exss)
	| null exss = Right "Matrix has no rows."
	| null $ head exss = Right "Matrix has no columns."
	| allRowsHaveSameColumnsAndSpace = Left $ S.Matrix rows columns t
	| otherwise = Right "Not all rows have the same number of columns or the same value types."
	where
	rows = length exss
	columns = if rows > 0 then length $ head exss else 0
	sss = map (map (infer cxt)) exss
	expT = head $ head sss
	allRowsHaveSameColumnsAndSpace
	= either
	(\_ -> all (\ r -> length r == columns && all (== expT) r) sss)
	(const False) expT
	t = fromLeft (error "Infer on Matrix had a strong expectation of Left-valued data.") expT -- This error should never occur.
	infer cxt (UnaryOp uf ex) = case infer cxt ex of
	Left sp -> case uf of
	Abs -> if S.isBasicNumSpace sp && sp /= S.Natural
	then Left sp
	else Right $ "Numeric 'absolute' value operator only applies to, non-natural, numeric types. Received `" ++ show sp ++ "`."
	Neg -> if S.isBasicNumSpace sp && sp /= S.Natural
	then Left sp
	else Right $ "Negation only applies to, non-natural, numeric types. Received `" ++ show sp ++ "`."
	Exp -> if sp == S.Real || sp == S.Integer then Left S.Real else Right $ show Exp ++ " only applies to reals."
	x -> if sp == S.Real
	then Left S.Real
	else Right $ show x ++ " only applies to Reals. Received `" ++ show sp ++ "`."
	x -> x
	infer cxt (UnaryOpB Not ex) = case infer cxt ex of
	Left S.Boolean -> Left S.Boolean
	Left sp -> Right $ "¬ on non-boolean operand, " ++ show sp ++ "."
	x -> x
	infer cxt (UnaryOpVV NegV e) = case infer cxt e of
	Left (S.Vect sp) -> if S.isBasicNumSpace sp && sp /= S.Natural
	then Left $ S.Vect sp
	else Right $ "Vector negation only applies to, non-natural, numbered vectors. Received `" ++ show sp ++ "`."
	Left sp -> Right $ "Vector negation should only be applied to numeric vectors. Received `" ++ show sp ++ "`."
	x -> x
	infer cxt (UnaryOpVN Norm e) = case infer cxt e of
	Left (S.Vect S.Real) -> Left S.Real
	Left sp -> Right $ "Vector norm only applies to vectors of real numbers. Received `" ++ show sp ++ "`."
	x -> x
	infer cxt (UnaryOpVN Dim e) = case infer cxt e of
	Left (S.Vect _) -> Left S.Integer -- FIXME: I feel like Integer would be more usable, but S.Natural is the 'real' expectation here
	Left sp -> Right $ "Vector 'dim' only applies to vectors. Received `" ++ show sp ++ "`."
	x -> x
	infer cxt (ArithBinaryOp Frac l r) = case (infer cxt l, infer cxt r) of
	(Left lt, Left rt) -> if S.isBasicNumSpace lt && lt == rt
	then Left lt
	else Right $ "Fractions/divisions should only be applied to the same numeric typed operands. Received `" ++ show lt ++ "` / `" ++ show rt ++ "`."
	(_ , Right e) -> Right e
	(Right e, _ ) -> Right e
	infer cxt (ArithBinaryOp Pow l r) = case (infer cxt l, infer cxt r) of
	(Left lt, Left rt) -> if S.isBasicNumSpace lt && (lt == rt || (lt == S.Real && rt == S.Integer))
	then Left lt
	else Right $
	"Powers should only be applied to the same numeric type in both operands, or real base with integer exponent. Received `" ++ show lt ++ "` ^ `" ++ show rt ++ "`."
	(_ , Right x) -> Right x
	(Right x, _ ) -> Right x
	infer cxt (ArithBinaryOp Subt l r) = case (infer cxt l, infer cxt r) of
	(Left lt, Left rt) -> if S.isBasicNumSpace lt && lt == rt
	then Left lt
	else Right $ "Both operands of a subtraction must be the same numeric type. Received `" ++ show lt ++ "` - `" ++ show rt ++ "`."
	(_, Right re) -> Right re
	(Right le, _) -> Right le
	infer cxt (BoolBinaryOp _ l r) = case (infer cxt l, infer cxt r) of
	(Left S.Boolean, Left S.Boolean) -> Left S.Boolean
	(Left lt, Left rt) -> Right $ "Boolean expression contains non-boolean operand. Received `" ++ show lt ++ "` & `" ++ show rt ++ "`."
	(_ , Right er) -> Right er
	(Right el, _ ) -> Right el
	infer cxt (EqBinaryOp _ l r) = case (infer cxt l, infer cxt r) of
	(Left lt, Left rt) -> if lt == rt
	then Left S.Boolean
	else Right $ "Both operands of an (in)equality (=/≠) must be of the same type. Received `" ++ show lt ++ "` & `" ++ show rt ++ "`."
	(_, Right re) -> Right re
	(Right le, _) -> Right le
	infer cxt (LABinaryOp Index l n) = case (infer cxt l, infer cxt n) of
	(Left (S.Vect lt), Left nt) -> if nt == S.Integer || nt == S.Natural -- I guess we should only want it to be natural numbers, but integers or naturals is fine for now
	then Left lt
	else Right $ "List accessor not of type Integer nor Natural, but of type `" ++ show nt ++ "`"
	(Left lt , Left _) -> Right $ "List accessor expects a list/vector, but received `" ++ show lt ++ "`."
	(_ , Right e) -> Right e
	(Right e , _ ) -> Right e
	infer cxt (OrdBinaryOp _ l r) = case (infer cxt l, infer cxt r) of
	(Left lt, Left rt) -> if S.isBasicNumSpace lt && lt == rt
	then Left S.Boolean
	else Right $ "Both operands of a numeric comparison must be the same numeric type, got: " ++ show lt ++ ", " ++ show rt ++ "."
	(_, Right re) -> Right re
	(Right le, _) -> Right le
	infer cxt (VVVBinaryOp o l r) = vvvInfer cxt o l r
	{- case (infer cxt l, infer cxt r) of
	(Left lTy, Left rTy) -> if lTy == rTy && S.isBasicNumSpace lTy && lTy /= S.Natural
	then Left lTy
	else Right $ "Vector cross product expects both operands to be vectors of non-natural numbers. Received `" ++ show lTy ++ "` X `" ++ show rTy ++ "`."
	(_ , Right re) -> Right re
	(Right le, _ ) -> Right le
	-}
	infer cxt (VVNBinaryOp Dot l r) = case (infer cxt l, infer cxt r) of
	(Left lt@(S.Vect lsp), Left rt@(S.Vect rsp)) -> if lsp == rsp && S.isBasicNumSpace lsp
	then Left lsp
	else Right $ "Vector dot product expects same numeric vector types, but found `" ++ show lt ++ "` · `" ++ show rt ++ "`."
	(Left lsp, Left rsp) -> Right $ "Vector dot product expects vector operands. Received `" ++ show lsp ++ "` · `" ++ show rsp ++ "`."
	(_, Right rx) -> Right rx
	(Right lx, _) -> Right lx
	infer cxt (NVVBinaryOp Scale l r) = case (infer cxt l, infer cxt r) of
	(Left lt, Left (S.Vect rsp)) -> if S.isBasicNumSpace lt && lt == rsp
	then Left rsp
	else if lt /= rsp then
	Right $ "Vector scaling expects a scaling by the same kind as the vector's but found scaling by`" ++ show lt ++ "` over vectors of type `" ++ show rsp ++ "`."
	else
	Right $ "Vector scaling expects a numeric scaling, but found `" ++ show lt ++ "`."
	(Left _, Left rsp) -> Right $ "Vector scaling expects vector as second operand. Received `" ++ show rsp ++ "`."
	(_, Right rx) -> Right rx
	(Right lx, _) -> Right lx
	infer cxt (Operator aao (S.BoundedDD _ _ bot top) body) =
	let expTy = assocArithOperToTy aao in
	case (infer cxt bot, infer cxt top, infer cxt body) of
	(Left botTy, Left topTy, Left bodyTy) -> if botTy == S.Integer
	then if topTy == S.Integer
	then if expTy == bodyTy
	then Left expTy
	else Right $ "'Big' operator range body not Integer, found: " ++ show bodyTy ++ "."
	else Right $ "'Big' operator range top not Integer, found: " ++ show topTy ++ "."
	else Right $ "'Big' operator range bottom not of expected type: " ++ show expTy ++ ", found: " ++ show botTy ++ "."
	(_ , _ , Right x ) -> Right x
	(_ , Right x , _ ) -> Right x
	(Right x , _ , _ ) -> Right x
	infer cxt (RealI uid ri) =
	case (inferFromContext cxt uid, riTy ri) of
	(Left S.Real, Left riSp) -> if riSp == S.Real
	then Left S.Boolean
	else Right $
	"Real interval expects interval bounds to be of type Real, but received: " ++ show riSp ++ "."
	(Left uidSp, _ ) -> Right $
	"Real interval expects variable to be of type Real, but received `" ++ show uid ++ "` of type `" ++ show uidSp ++ "`."
	(_ , Right x ) -> Right x
	(Right x , _ ) -> Right x
	where
	riTy :: RealInterval Expr Expr -> Either Space TypeError
	riTy (S.Bounded (_, lx) (_, rx)) = case (infer cxt lx, infer cxt rx) of
	(Left lt, Left rt) -> if lt == rt
	then Left lt
	else Right $
	"Bounded real interval contains mismatched types for bottom and top. Received `" ++ show lt ++ "` to `" ++ show rt ++ "`."
	(_ , Right x) -> Right x
	(Right x, _ ) -> Right x
	riTy (S.UpTo (_, x)) = infer cxt x
	riTy (S.UpFrom (_, x)) = infer cxt x

Issues with the current work

We see:

1. The code is very verbose and hard to read.
2. Error messages are somewhat okay, but lack the majority of the contextual information for users to debug where a type error occurred.
3. A lot of code duplication.

Ultimately, there's a lot of room for improvement.

What we want

First, we want the inverse of the 3 issues:

1. Easier to read, shorter code.
2. Better type error messages.
3. Less code duplication.

Afterwards, we want to extend the type-checker to ModelExpr and CodeExpr, while being mindful of code duplication. ModelExpr will be a bit more complicated than extension to CodeExpr because of a non-trivial interest: type variables.

Where should we go?

For now, we will focus on the earlier 3 issues.

To address the first issue and the parts of the third, I think we can switch over to a monadic type inference system. Right now, monads are severely underused. We can review how much code duplication is left over after switching to a monadic style.

Now, for improved type error messages, I'm not completely sure. One thing is for sure: we need to be able to track where we are in the expression as we go along. Do we do that from “source”? I don't see any easy way to do that without writing a GHC plugin, but I'm not sure if that's the route we want to go down. So, should we track just the AST and print out a horizontal tree that prints the AST with the root in the right-most position? Should we just try to print out Haskell-like code? I'm not quite sure.

[smiths]

Nice summary @balacij. I don't know the answers to your questions, but @JacquesCarette very likely will have some thoughts. Maybe we should discuss this during our morning meeting on Monday?

[balacij]

Thank you! Hmm, I don't think it would hurt, but I think this one can be done over GitHub, so perhaps as a lower priority item?

[JacquesCarette]

As discussed today, we also want the code to "look like" the typing rules as much as possible.

One of the things to do to clean up the code a lot is to move the error-generating code "elsewhere". And error happens when a conflict arises between reality (the Expr) and one of the rules (in context). So given the inputs to check (or infer) and the detected conflict then a completely separate routine should be able to reconstruct the error.

Then the remaining work becomes one of 'classifying' the different kinds of conflicts that can arise from the rules.

I wonder if there's something we can learn from Andrej Bauer's PL zoo regarding this.