Swarm.Language.Typecheck

Type inference for the Swarm language. For the approach used here, see https://byorgey.wordpress.com/2021/09/08/implementing-hindley-milner-with-the-unification-fd-library/ .

Type errors

data ContextualTypeErr

A type error along with various contextual information to help us generate better error messages.

Constructors

CTE

Fields

• cteSrcLoc :: SrcLoc
• cteStack :: TCStack
• cteTypeErr :: TypeErr

Instances

Show ContextualTypeErr

Defined in Swarm.Language.Typecheck

Methods

showsPrec :: Int -> ContextualTypeErr -> ShowS

show :: ContextualTypeErr -> String

showList :: [ContextualTypeErr] -> ShowS

data TypeErr

Errors that can occur during type checking. The idea is that each error carries information that can be used to help explain what went wrong (though the amount of information carried can and should be very much improved in the future); errors can then separately be pretty-printed to display them to the user.

Constructors

UnboundVar Var

An undefined variable was encountered.

KindErr KindError

A kind error was encountered.

EscapedSkolem Var

A Skolem variable escaped its local context.

UnificationErr UnificationError

Occurs check failure, i.e. infinite type.

Mismatch (Maybe Syntax) TypeJoin

Type mismatch caught by unify. The given term was expected to have a certain type, but has a different type instead.

LambdaArgMismatch TypeJoin

Lambda argument type mismatch.

FieldsMismatch (Join (Set Var))

Record field mismatch, i.e. based on the expected type we were expecting a record with certain fields, but found one with a different field set.

DefNotTopLevel Term

A definition was encountered not at the top level.

CantInfer Term

A term was encountered which we cannot infer the type of. This should never happen.

CantInferProj Term

We can't infer the type of a record projection r.x if we don't concretely know the type of the record r.

UnknownProj Var Term

An attempt to project out a nonexistent field

InvalidAtomic InvalidAtomicReason Term

An invalid argument was provided to atomic.

Impredicative

Some unification variables ended up in a type, probably due to impredicativity. See https://github.com/swarm-game/swarm/issues/351 .

Instances

Show TypeErr

Defined in Swarm.Language.Typecheck

Methods

showsPrec :: Int -> TypeErr -> ShowS

show :: TypeErr -> String

showList :: [TypeErr] -> ShowS

PrettyPrec TypeErr

Defined in Swarm.Language.Pretty

Methods

prettyPrec :: Int -> TypeErr -> Doc ann

data InvalidAtomicReason

Various reasons the body of an atomic might be invalid.

Constructors

TooManyTicks Int

The argument has too many tangible commands.

AtomicDupingThing

The argument uses some way to duplicate code: def, let, or lambda.

NonSimpleVarType Var UPolytype

The argument referred to a variable with a non-simple type.

NestedAtomic

The argument had a nested atomic

LongConst

The argument contained a long command

AtomicSuspend

The argument contained a suspend

Instances

Show InvalidAtomicReason

Defined in Swarm.Language.Typecheck

Methods

showsPrec :: Int -> InvalidAtomicReason -> ShowS

show :: InvalidAtomicReason -> String

showList :: [InvalidAtomicReason] -> ShowS

PrettyPrec InvalidAtomicReason

Defined in Swarm.Language.Pretty

Methods

prettyPrec :: Int -> InvalidAtomicReason -> Doc ann

Type provenance

data Source

The source of a type during typechecking.

Constructors

Expected

An expected type that was "pushed down" from the context.

Actual

An actual/inferred type that was "pulled up" from a term.

Instances

Bounded Source

Defined in Swarm.Language.Typecheck

Methods

minBound :: Source

maxBound :: Source

Enum Source

Defined in Swarm.Language.Typecheck

Methods

succ :: Source -> Source

pred :: Source -> Source

toEnum :: Int -> Source

fromEnum :: Source -> Int

enumFrom :: Source -> [Source]

enumFromThen :: Source -> Source -> [Source]

enumFromTo :: Source -> Source -> [Source]

enumFromThenTo :: Source -> Source -> Source -> [Source]

Show Source

Defined in Swarm.Language.Typecheck

Methods

showsPrec :: Int -> Source -> ShowS

show :: Source -> String

showList :: [Source] -> ShowS

Eq Source

Defined in Swarm.Language.Typecheck

Methods

(==) :: Source -> Source -> Bool

(/=) :: Source -> Source -> Bool

Ord Source

Defined in Swarm.Language.Typecheck

Methods

compare :: Source -> Source -> Ordering

(<) :: Source -> Source -> Bool

(<=) :: Source -> Source -> Bool

(>) :: Source -> Source -> Bool

(>=) :: Source -> Source -> Bool

max :: Source -> Source -> Source

min :: Source -> Source -> Source

withSource :: Source -> a -> a -> a

Generic eliminator for Source. Choose the first argument if the Source is Expected, and the second argument if Actual.

data Join a

A "join" where an expected thing meets an actual thing.

Instances

Foldable Join

Defined in Swarm.Language.Typecheck

Methods

fold :: Monoid m => Join m -> m

foldMap :: Monoid m => (a -> m) -> Join a -> m

foldMap' :: Monoid m => (a -> m) -> Join a -> m

foldr :: (a -> b -> b) -> b -> Join a -> b

foldr' :: (a -> b -> b) -> b -> Join a -> b

foldl :: (b -> a -> b) -> b -> Join a -> b

foldl' :: (b -> a -> b) -> b -> Join a -> b

foldr1 :: (a -> a -> a) -> Join a -> a

foldl1 :: (a -> a -> a) -> Join a -> a

toList :: Join a -> [a]

null :: Join a -> Bool

length :: Join a -> Int

elem :: Eq a => a -> Join a -> Bool

maximum :: Ord a => Join a -> a

minimum :: Ord a => Join a -> a

sum :: Num a => Join a -> a

product :: Num a => Join a -> a

Traversable Join

Defined in Swarm.Language.Typecheck

Methods

traverse :: Applicative f => (a -> f b) -> Join a -> f (Join b)

sequenceA :: Applicative f => Join (f a) -> f (Join a)

mapM :: Monad m => (a -> m b) -> Join a -> m (Join b)

sequence :: Monad m => Join (m a) -> m (Join a)

Functor Join

Defined in Swarm.Language.Typecheck

Methods

fmap :: (a -> b) -> Join a -> Join b

(<$) :: a -> Join b -> Join a

Show a => Show (Join a)

Defined in Swarm.Language.Typecheck

Methods

showsPrec :: Int -> Join a -> ShowS

show :: Join a -> String

showList :: [Join a] -> ShowS

getJoin :: Join a -> (a, a)

Convert a Join into a pair of (expected, actual).

Typechecking stack

data TCFrame where

A frame to keep track of something we were in the middle of doing during typechecking.

Constructors

TCLet :: Var -> TCFrame

Checking a definition.

TCBindL :: TCFrame

Inferring the LHS of a bind.

TCBindR :: TCFrame

Inferring the RHS of a bind.

Instances

Show TCFrame

Defined in Swarm.Language.Typecheck

Methods

showsPrec :: Int -> TCFrame -> ShowS

show :: TCFrame -> String

showList :: [TCFrame] -> ShowS

PrettyPrec TCFrame

Defined in Swarm.Language.Pretty

Methods

prettyPrec :: Int -> TCFrame -> Doc ann

data LocatedTCFrame

A typechecking stack frame together with the relevant SrcLoc.

Constructors

LocatedTCFrame SrcLoc TCFrame

Instances

Show LocatedTCFrame

Defined in Swarm.Language.Typecheck

Methods

showsPrec :: Int -> LocatedTCFrame -> ShowS

show :: LocatedTCFrame -> String

showList :: [LocatedTCFrame] -> ShowS

PrettyPrec LocatedTCFrame

Defined in Swarm.Language.Pretty

Methods

prettyPrec :: Int -> LocatedTCFrame -> Doc ann

type TCStack = [LocatedTCFrame]

A typechecking stack keeps track of what we are currently in the middle of doing during typechecking.

withFrame :: Has (Reader TCStack) sig m => SrcLoc -> TCFrame -> m a -> m a

Push a frame on the typechecking stack.

Typechecking monad

fresh :: Has Unification sig m => m UType

Generate a fresh unification variable.

Unification

instantiate :: Has Unification sig m => UPolytype -> m UType

To instantiate a UPolytype, we generate a fresh unification variable for each variable bound by the Forall, and then substitute them throughout the type.

skolemize :: Has Unification sig m => UPolytype -> m UType

skolemize is like instantiate, except we substitute fresh type variables instead of unification variables. Such variables cannot unify with anything other than themselves. This is used when checking something with a polytype explicitly specified by the user.

generalize :: (Has Unification sig m, Has (Reader UCtx) sig m) => UType -> m UPolytype

generalize is the opposite of instantiate: add a Forall which closes over all free type and unification variables.

Pick nice type variable names instead of reusing whatever fresh names happened to be used for the free variables.

Type inference

inferTop :: TCtx -> ReqCtx -> TDCtx -> Syntax -> Either ContextualTypeErr TSyntax

Top-level type inference function: given a context of definition types, type synonyms, and a term, either return a type error or a fully type-annotated version of the term.

infer :: (Has (Reader UCtx) sig m, Has (Reader ReqCtx) sig m, Has (Reader TDCtx) sig m, Has (Reader TCStack) sig m, Has Unification sig m, Has (Error ContextualTypeErr) sig m) => Syntax -> m (Syntax' UType)

Infer the type of a term, returning a type-annotated term.

The only cases explicitly handled in infer are those where pushing an expected type down into the term can't possibly help, e.g. most primitives, function application, and binds.

For most everything else we prefer check because it can often result in better and more localized type error messages.

Note that we choose to do kind checking inline as we go during typechecking. This has pros and cons. The benefit is that we get to piggyback on the existing source location tracking and typechecking stack, so we can generate better error messages. The downside is that we have to be really careful not to miss any types along the way; there is no difference, at the Haskell type level, between ill- and well-kinded Swarm types, so we just have to make sure that we call checkKind on every type embedded in the term being checked.

inferConst :: Const -> Polytype

Infer the type of a constant.

check :: (Has (Reader UCtx) sig m, Has (Reader ReqCtx) sig m, Has (Reader TDCtx) sig m, Has (Reader TCStack) sig m, Has Unification sig m, Has (Error ContextualTypeErr) sig m) => Syntax -> UType -> m (Syntax' UType)

check t ty checks that t has type ty, returning a type-annotated AST if so.

We try to stay in checking mode as far as possible, decomposing the expected type as we go and pushing it through the recursion.

isSimpleUType :: UType -> Bool

A simple type is a sum or product of base types.