License | BSD-3-Clause |
---|---|
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 ContextualTypeErr = CTE {}
- data TypeErr
- = UnboundVar Var
- | EscapedSkolem Var
- | Infinite IntVar UType
- | UnifyErr (TypeF UType) (TypeF UType)
- | Mismatch (Maybe Syntax) TypeJoin
- | LambdaArgMismatch TypeJoin
- | FieldsMismatch (Join (Set Var))
- | DefNotTopLevel Term
- | CantInfer Term
- | CantInferProj Term
- | UnknownProj Var Term
- | InvalidAtomic InvalidAtomicReason Term
- | Impredicative
- data InvalidAtomicReason
- data Source
- withSource :: Source -> a -> a -> a
- data Join a
- getJoin :: Join a -> (a, a)
- data TCFrame where
- data LocatedTCFrame = LocatedTCFrame SrcLoc TCFrame
- type TCStack = [LocatedTCFrame]
- withFrame :: SrcLoc -> TCFrame -> TC a -> TC a
- getTCStack :: TC TCStack
- type TC = ReaderT UCtx (ReaderT TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
- runTC :: TCtx -> TC UModule -> Either ContextualTypeErr TModule
- fresh :: TC UType
- substU :: Map (Either Var IntVar) UType -> UType -> UType
- unify :: Maybe Syntax -> TypeJoin -> TC UType
- class HasBindings u where
- applyBindings :: u -> TC u
- instantiate :: UPolytype -> TC UType
- skolemize :: UPolytype -> TC UType
- generalize :: UType -> TC UPolytype
- inferTop :: TCtx -> Syntax -> Either ContextualTypeErr TModule
- inferModule :: Syntax -> TC UModule
- infer :: Syntax -> TC (Syntax' UType)
- inferConst :: Const -> Polytype
- check :: Syntax -> UType -> TC (Syntax' UType)
- isSimpleUType :: UType -> Bool
Type errors
data ContextualTypeErr Source #
A type error along with various contextual information to help us generate better error messages.
Instances
Show ContextualTypeErr Source # | |
Defined in Swarm.Language.Typecheck showsPrec :: Int -> ContextualTypeErr -> ShowS # show :: ContextualTypeErr -> String # showList :: [ContextualTypeErr] -> ShowS # | |
Fallible TypeF IntVar ContextualTypeErr Source # | |
Defined in Swarm.Language.Typecheck occursFailure :: IntVar -> UTerm TypeF IntVar -> ContextualTypeErr # mismatchFailure :: TypeF (UTerm TypeF IntVar) -> TypeF (UTerm TypeF IntVar) -> ContextualTypeErr # |
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 Var | An undefined variable was encountered. |
EscapedSkolem Var | A Skolem variable escaped its local context. |
Infinite IntVar UType | Occurs check failure, i.e. infinite type. |
UnifyErr (TypeF UType) (TypeF UType) | Error generated by the unifier. |
Mismatch (Maybe Syntax) TypeJoin | Type mismatch caught by |
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 |
UnknownProj Var Term | An attempt to project out a nonexistent field |
InvalidAtomic InvalidAtomicReason Term | An invalid argument was provided to |
Impredicative | Some unification variables ended up in a type, probably due to impredicativity. See https://github.com/swarm-game/swarm/issues/351 . |
data InvalidAtomicReason Source #
Various reasons the body of an atomic
might be invalid.
TooManyTicks Int | The argument 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 # |
Type provenance
The source of a type during typechecking.
Expected | An expected type that was "pushed down" from the context. |
Actual | An actual/inferred type that was "pulled up" from a term. |
withSource :: Source -> a -> a -> a Source #
A "join" where an expected thing meets an actual thing.
Typechecking stack
A frame to keep track of something we were in the middle of doing during typechecking.
data LocatedTCFrame Source #
A typechecking stack frame together with the relevant SrcLoc
.
Instances
Show LocatedTCFrame Source # | |
Defined in Swarm.Language.Typecheck showsPrec :: Int -> LocatedTCFrame -> ShowS # show :: LocatedTCFrame -> String # showList :: [LocatedTCFrame] -> ShowS # | |
PrettyPrec LocatedTCFrame Source # | |
Defined in Swarm.Language.Pretty prettyPrec :: Int -> LocatedTCFrame -> Doc ann Source # |
type TCStack = [LocatedTCFrame] Source #
A typechecking stack keeps track of what we are currently in the middle of doing during typechecking.
withFrame :: SrcLoc -> TCFrame -> TC a -> TC a Source #
Push a frame on the typechecking stack within a local TC
computation.
getTCStack :: TC TCStack Source #
Get the current typechecking stack.
Typechecking monad
type TC = ReaderT UCtx (ReaderT TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity))) Source #
The concrete monad used for type checking. IntBindingT
is a
monad transformer provided by the unification-fd
library which
supports various operations such as generating fresh variables
and unifying things.
Unification
unify :: Maybe Syntax -> TypeJoin -> TC UType Source #
unify t expTy actTy
ensures that the given two types are equal.
If we know the actual term t
which is supposed to have these
types, we can use it to generate better error messages.
We first do a quick-and-dirty check to see whether we know for sure the types either are or cannot be equal, generating an equality constraint for the unifier as a last resort.
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 -> TC u Source #
Instances
HasBindings UModule Source # | |
Defined in Swarm.Language.Typecheck | |
HasBindings UCtx Source # | |
Defined in Swarm.Language.Typecheck | |
HasBindings UPolytype Source # | |
Defined in Swarm.Language.Typecheck | |
HasBindings UType Source # | |
Defined in Swarm.Language.Typecheck | |
(HasBindings u, Data u) => HasBindings (Syntax' u) Source # | |
Defined in Swarm.Language.Typecheck | |
(HasBindings u, Data u) => HasBindings (Term' u) Source # | |
Defined in Swarm.Language.Typecheck |
instantiate :: UPolytype -> TC 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 -> TC 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 -> TC UPolytype Source #
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 -> Syntax -> Either ContextualTypeErr 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 -> TC UModule Source #
Infer the signature of a top-level expression which might contain definitions.
infer :: Syntax -> TC (Syntax' UType) Source #
Infer the type of a term which does not contain definitions, 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.
inferConst :: Const -> Polytype Source #
Infer the type of a constant.
check :: Syntax -> UType -> TC (Syntax' UType) Source #
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 Source #
A simple type is a sum or product of base types.