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 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 Location Var

An undefined variable was encountered.

EscapedSkolem Location Var

A Skolem variable escaped its local context.

Infinite IntVar UType

Mismatch Location (TypeF UType) (TypeF UType)

The given term was expected to have a certain type, but has a different type instead.

DefNotTopLevel Location Term

A definition was encountered not at the top level.

CantInfer Location Term

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

InvalidAtomic Location InvalidAtomicReason Term

An invalid argument was provided to atomic.

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

Fallible TypeF IntVar TypeErr

Defined in Swarm.Language.Typecheck

Methods

occursFailure :: IntVar -> UTerm TypeF IntVar -> TypeErr

mismatchFailure :: TypeF (UTerm TypeF IntVar) -> TypeF (UTerm TypeF IntVar) -> TypeErr

data InvalidAtomicReason

Various reasons the body of an atomic might be invalid.

Constructors

TooManyTicks Int

The arugment 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

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

getTypeErrLocation :: TypeErr -> Maybe Location

Inference monad

type Infer = ReaderT UCtx (ExceptT TypeErr (IntBindingT TypeF Identity))

The concrete monad used for type inference. IntBindingT is a monad transformer provided by the unification-fd library which supports various operations such as generating fresh variables and unifying things.

runInfer :: TCtx -> Infer UModule -> Either TypeErr TModule

Run a top-level inference computation, returning either a TypeErr or a fully resolved TModule.

lookup :: Location -> Var -> Infer UType

Look up a variable in the ambient type context, either throwing an UnboundVar error if it is not found, or opening its associated UPolytype with fresh unification variables via instantiate.

fresh :: Infer UType

Generate a fresh unification variable.

Unification

substU :: Map (Either Var IntVar) UType -> UType -> UType

Perform a substitution over a UType, substituting for both type and unification variables. Note that since UTypes do not have any binding constructs, we don't have to worry about ignoring bound variables; all variables in a UType are free.

(=:=) :: UType -> UType -> Infer () infix 4

Constrain two types to be equal.

class HasBindings u where

unification-fd provides a function applyBindings which fully substitutes for any bound unification variables (for efficiency, it does not perform such substitution as it goes along). The HasBindings class is for anything which has unification variables in it and to which we can usefully apply applyBindings.

Methods

applyBindings :: u -> Infer u

Instances

HasBindings UCtx

Defined in Swarm.Language.Typecheck

Methods

applyBindings :: UCtx -> Infer UCtx

HasBindings UModule

Defined in Swarm.Language.Typecheck

Methods

applyBindings :: UModule -> Infer UModule

HasBindings UPolytype

Defined in Swarm.Language.Typecheck

Methods

applyBindings :: UPolytype -> Infer UPolytype

HasBindings UType

Defined in Swarm.Language.Typecheck

Methods

applyBindings :: UType -> Infer UType

instantiate :: UPolytype -> Infer 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 :: UPolytype -> Infer 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 :: UType -> Infer UPolytype

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

Type inference

inferTop :: TCtx -> Syntax -> Either TypeErr TModule

Top-level type inference function: given a context of definition types and a top-level term, either return a type error or its type as a TModule.

inferModule :: Syntax -> Infer UModule

Infer the signature of a top-level expression which might contain definitions.

infer :: Syntax -> Infer UType

Infer the type of a term which does not contain definitions.

inferConst :: Const -> Polytype

Infer the type of a constant.

check :: Syntax -> UType -> Infer ()

check t ty checks that t has type ty.

decomposeCmdTy :: UType -> Infer UType

Decompose a type that is supposed to be a command type.

decomposeFunTy :: UType -> Infer (UType, UType)

Decompose a type that is supposed to be a function type.

isSimpleUType :: UType -> Bool

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

Orphan instances

Ord IntVar

unification-fd does not provide an Ord instance for IntVar, so we must provide our own, in order to be able to store IntVars in a Set.

Methods

compare :: IntVar -> IntVar -> Ordering

(<) :: IntVar -> IntVar -> Bool

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

(>) :: IntVar -> IntVar -> Bool

(>=) :: IntVar -> IntVar -> Bool

max :: IntVar -> IntVar -> IntVar

min :: IntVar -> IntVar -> IntVar