| Copyright | (c) Kimiyuki Onaka 2021 |
|---|---|
| License | Apache License 2.0 |
| Maintainer | kimiyuki95@gmail.com |
| Stability | experimental |
| Portability | portable |
| Safe Haskell | None |
| Language | Haskell2010 |
Jikka.RestrictedPython.Convert.TypeInfer
Contents
Description
Synopsis
- run :: (MonadAlpha m, MonadError Error m) => Program -> m Program
- data Equation
- formularizeProgram :: MonadAlpha m => Program -> m [Equation]
- sortEquations :: [Equation] -> ([(Type, Type, Maybe Loc)], [(VarName', Type)])
- mergeAssertions :: [(VarName', Type)] -> [(Type, Type, Maybe Loc)]
- newtype Subst = Subst {}
- subst :: Subst -> Type -> Type
- solveEquations :: MonadError Error m => [(Type, Type, Maybe Loc)] -> m Subst
- mapTypeProgram :: (Type -> Type) -> Program -> Program
Documentation
run :: (MonadAlpha m, MonadError Error m) => Program -> m Program Source #
run infers types of given programs.
As the interface, you can understand this function does the following:
- Finds a type environment \(\Gamma\) s.t. for all statement \(\mathrm{stmt}\) in the given program, \(\Gamma \vdash \mathrm{stmt}\) holds, and
- Annotates each variable in the program using the \(\Gamma\).
In its implementation, this is just something like a Hindley-Milner type inference.
Requirements
- There must be no name conflicts in given programs. They must be alpha-converted. (
Alpha) - All names must be resolved. (
ResolveBuiltin)
internal types and functions
Constructors
| TypeEquation Type Type (Maybe Loc) | |
| TypeAssertion VarName' Type |
formularizeProgram :: MonadAlpha m => Program -> m [Equation] Source #
Subst is type substituion. It's a mapping from type variables to their actual types.
solveEquations :: MonadError Error m => [(Type, Type, Maybe Loc)] -> m Subst Source #