Copyright | Brent Yorgey |
---|---|
License | BSD-3-Clause |
Maintainer | byorgey@gmail.com |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
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/ .
Synopsis
- data TypeErr
- data InvalidAtomicReason
- getTypeErrLocation :: TypeErr -> Maybe Location
- type Infer = ReaderT UCtx (ExceptT TypeErr (IntBindingT TypeF Identity))
- runInfer :: TCtx -> Infer UModule -> Either TypeErr TModule
- lookup :: Location -> Var -> Infer UType
- fresh :: Infer UType
- substU :: Map (Either Var IntVar) UType -> UType -> UType
- (=:=) :: UType -> UType -> Infer ()
- class HasBindings u where
- applyBindings :: u -> Infer u
- instantiate :: UPolytype -> Infer UType
- skolemize :: UPolytype -> Infer UType
- generalize :: UType -> Infer UPolytype
- inferTop :: TCtx -> Syntax -> Either TypeErr TModule
- inferModule :: Syntax -> Infer UModule
- infer :: Syntax -> Infer UType
- inferConst :: Const -> Polytype
- check :: Syntax -> UType -> Infer ()
- decomposeCmdTy :: UType -> Infer UType
- decomposeFunTy :: UType -> Infer (UType, UType)
- isSimpleUType :: UType -> Bool
Type errors
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.
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 |
data InvalidAtomicReason Source #
Various reasons the body of an atomic
might be invalid.
TooManyTicks Int | The arugment has too many tangible commands. |
AtomicDupingThing | The argument uses some way to duplicate code: |
NonSimpleVarType Var UPolytype | The argument referred to a variable with a non-simple type. |
NestedAtomic | The argument had a nested |
LongConst | The argument contained a long command |
Instances
Show InvalidAtomicReason Source # | |
Defined in Swarm.Language.Typecheck showsPrec :: Int -> InvalidAtomicReason -> ShowS # show :: InvalidAtomicReason -> String # showList :: [InvalidAtomicReason] -> ShowS # | |
PrettyPrec InvalidAtomicReason Source # | |
Defined in Swarm.Language.Pretty prettyPrec :: Int -> InvalidAtomicReason -> Doc ann Source # |
Inference monad
type Infer = ReaderT UCtx (ExceptT TypeErr (IntBindingT TypeF Identity)) Source #
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.
lookup :: Location -> Var -> Infer UType Source #
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
.
Unification
class HasBindings u where Source #
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
.
applyBindings :: u -> Infer u Source #
Instances
HasBindings UCtx Source # | |
Defined in Swarm.Language.Typecheck | |
HasBindings UModule Source # | |
Defined in Swarm.Language.Typecheck | |
HasBindings UPolytype Source # | |
Defined in Swarm.Language.Typecheck | |
HasBindings UType Source # | |
Defined in Swarm.Language.Typecheck |
instantiate :: UPolytype -> Infer UType Source #
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 Source #
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 Source #
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 Source #
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 Source #
Infer the signature of a top-level expression which might contain definitions.
inferConst :: Const -> Polytype Source #
Infer the type of a constant.
decomposeCmdTy :: UType -> Infer UType Source #
Decompose a type that is supposed to be a command type.
decomposeFunTy :: UType -> Infer (UType, UType) Source #
Decompose a type that is supposed to be a function type.
isSimpleUType :: UType -> Bool Source #
A simple type is a sum or product of base types.