Safe Haskell	Safe-Inferred
Language	GHC2021

Language.Giml.Types.Infer.Elaborate

Contents

Elaborate data types
- Types
- Algorithm
Elaborate

Description

Elaborate types

During the elaboration phase we annotate the AST with the types we know. When we don't know what the type of something is, we generate a new type variable as a placeholder and mark that type with a Constraint depending on its syntactic use.

Input: Builtin data types, builtin type environment, and the AST
Output: Annotated AST with types (to the best of our abilities) + constraints on those types

Synopsis

type ElaborateData b m = (MonadBase b m, MonadState VariantEnv m, MonadError TypeErrorA m)
data ElabState = ElabState {
- esTypeVarCounter :: Int
- esConstraints :: Constraints
}
data ElabEnv b = ElabEnv {
- eeTypeEnv :: Env Type
- eeBuiltins :: Env Type
- eeVariantEnv :: VariantEnv
- logAction :: LogAction b LogMsg
}
elaborateEnv :: MonadBase b b => [Datatype ()] -> [Datatype InputAnn] -> ExceptT TypeErrorA b ([Datatype Ann], VariantEnv)
addVariantSigs :: ElaborateData b m => VariantEnv -> m ()
elaborateTypeDef :: ElaborateData b m => Datatype InputAnn -> m (Datatype Ann)
elaborate :: MonadBase b b => LogAction b LogMsg -> VariantEnv -> Env Type -> [TermDef InputAnn] -> ExceptT TypeErrorA b ([TermDef Ann], ElabState)
type Elaborate b m = (MonadBase b m, MonadState ElabState m, MonadReader (ElabEnv b) m, MonadError TypeErrorA m)
type Env a = Map Var a
type VariantEnv = Map Constr (VariantSig InputAnn)
data ElabInfo a = ElabInfo {
- eiResult :: a
- eiType :: Type
- eiNewEnv :: Env Type
}
lookupVarMaybe :: Elaborate b m => Var -> m (Maybe Type)
lookupVar :: Elaborate b m => InputAnn -> Var -> m Type
lookupBuiltin :: Elaborate b m => InputAnn -> Var -> m Type
insertToEnv :: Env Type -> ElabEnv b -> ElabEnv b
removeFromEnv :: [Var] -> ElabEnv b -> ElabEnv b
withEnv :: Elaborate b m => [(Var, Type)] -> m a -> m a
withEnv' :: Elaborate b m => Env Type -> m a -> m a
withoutEnv :: Elaborate b m => [Var] -> m a -> m a
lookupVariant :: Elaborate b m => InputAnn -> Constr -> m (VariantSig InputAnn)
genTypeVar :: MonadState ElabState m => Text -> m TypeVar
constrain :: Elaborate b m => InputAnn -> Constraint -> m ()
runElaborate :: MonadBase b b => LogAction b LogMsg -> VariantEnv -> Env Type -> [TermDef InputAnn] -> ExceptT TypeErrorA b ([TermDef Ann], ElabState)
elaborateFile :: Elaborate b m => [TermDef InputAnn] -> m [TermDef Ann]
elaborateDef :: Elaborate b m => TermDef InputAnn -> m (TermDef Ann)
elaborateTermDef :: Elaborate b m => TermDef InputAnn -> m (ElabInfo (TermDef Ann))
elaborateBlock :: Elaborate b m => Block InputAnn -> m (Type, Block Ann)
elaborateStmt :: Elaborate b m => Statement InputAnn -> m (ElabInfo (Statement Ann))
elaborateExpr :: Elaborate b m => InputAnn -> Expr InputAnn -> m (Expr Ann)
elaboratePatterns :: Elaborate b m => InputAnn -> Type -> Type -> [(Pattern, Expr InputAnn)] -> m [(Pattern, Expr Ann)]
elaboratePattern :: Elaborate b m => InputAnn -> TypeVar -> Pattern -> m [(Var, Type)]
getLitType :: Lit -> Type
type Solve b m = (MonadBase b m, MonadError TypeErrorA m, MonadState ElabState m, MonadReader (ElabEnv b) m)
instantiate :: Solve b m => Text -> [TypeVar] -> Type -> m Type

Elaborate data types

Types

type ElaborateData b m = (MonadBase b m, MonadState VariantEnv m, MonadError TypeErrorA m) Source #

The monadic capabilities for the elaboration phase.

data ElabState Source #

The state we keep during elaboration.

Constructors

ElabState
Fields esTypeVarCounter :: Int Used to generate unique type variable names. esConstraints :: Constraints The constraints we collect.

data ElabEnv b Source #

The environment we use.

Constructors

ElabEnv
Fields eeTypeEnv :: Env Type Represents the variables in scope and their types. eeBuiltins :: Env Type eeVariantEnv :: VariantEnv Mapping from a data constructor name to the data type and variant type signature. logAction :: LogAction b LogMsg

Instances

Instances details

Generic (ElabEnv b) Source #
Instance details Defined in Language.Giml.Types.Infer.Elaborate Associated Types type Rep (ElabEnv b) :: Type -> Type # Methods from :: ElabEnv b -> Rep (ElabEnv b) x # to :: Rep (ElabEnv b) x -> ElabEnv b #
type Rep (ElabEnv b) Source #
Instance details Defined in Language.Giml.Types.Infer.Elaborate type Rep (ElabEnv b) = D1 ('MetaData "ElabEnv" "Language.Giml.Types.Infer.Elaborate" "giml-transform-0.1.0.0-GJGU1pmFy2hE3zgdYhpK8b" 'False) (C1 ('MetaCons "ElabEnv" 'PrefixI 'True) ((S1 ('MetaSel ('Just "eeTypeEnv") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Env Type)) :: S1 ('MetaSel ('Just "eeBuiltins") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Env Type))) :: (S1 ('MetaSel ('Just "eeVariantEnv") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 VariantEnv) :*: S1 ('MetaSel ('Just "logAction") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (LogAction b LogMsg)))))

Algorithm

elaborateEnv :: MonadBase b b => [Datatype ()] -> [Datatype InputAnn] -> ExceptT TypeErrorA b ([Datatype Ann], VariantEnv) Source #

addVariantSigs :: ElaborateData b m => VariantEnv -> m () Source #

Add a datatype information into the environment

elaborateTypeDef :: ElaborateData b m => Datatype InputAnn -> m (Datatype Ann) Source #

Add a data type to the VariantEnv and elaborate it with a dummy type.

Elaborate

elaborate :: MonadBase b b => LogAction b LogMsg -> VariantEnv -> Env Type -> [TermDef InputAnn] -> ExceptT TypeErrorA b ([TermDef Ann], ElabState) Source #

Run elaboration algorithm

Types

type Elaborate b m = (MonadBase b m, MonadState ElabState m, MonadReader (ElabEnv b) m, MonadError TypeErrorA m) Source #

The monadic capabilities for the elaboration phase.

type Env a = Map Var a Source #

An environment from a name to something.

type VariantEnv = Map Constr (VariantSig InputAnn) Source #

A mapping from a data constructor to the type that defines it and the type it holds.

data ElabInfo a Source #

Return type for some elaboration functions.

Constructors

ElabInfo
Fields eiResult :: a The result of the current elaboration eiType :: Type The type of the result eiNewEnv :: Env Type A definition to add to the environment for the next statements, if needed.

Utils

lookupVarMaybe :: Elaborate b m => Var -> m (Maybe Type) Source #

Try to find the type of a variable in scope.

lookupVar :: Elaborate b m => InputAnn -> Var -> m Type Source #

Same as lookupVarMaybe but throws an UnboundVar error on failure.

lookupBuiltin :: Elaborate b m => InputAnn -> Var -> m Type Source #

Look for a builtin value/function. Throws an UnboundVar error on failure.

insertToEnv :: Env Type -> ElabEnv b -> ElabEnv b Source #

Adding new variable into the scope

removeFromEnv :: [Var] -> ElabEnv b -> ElabEnv b Source #

Remove variables from the scope

withEnv :: Elaborate b m => [(Var, Type)] -> m a -> m a Source #

Run an elaboration function with extra variables in scope.

withEnv' :: Elaborate b m => Env Type -> m a -> m a Source #

Run an elaboration function with extra variables in scope (Map version).

withoutEnv :: Elaborate b m => [Var] -> m a -> m a Source #

Run an elaboration function without some variables in scope.

lookupVariant :: Elaborate b m => InputAnn -> Constr -> m (VariantSig InputAnn) Source #

Lookup variant in env

genTypeVar :: MonadState ElabState m => Text -> m TypeVar Source #

Generate a new type variable.

constrain :: Elaborate b m => InputAnn -> Constraint -> m () Source #

Add a new constraint.

Algorithm

runElaborate :: MonadBase b b => LogAction b LogMsg -> VariantEnv -> Env Type -> [TermDef InputAnn] -> ExceptT TypeErrorA b ([TermDef Ann], ElabState) Source #

Run the algorithm.

elaborateFile :: Elaborate b m => [TermDef InputAnn] -> m [TermDef Ann] Source #

Elaborate a source file

elaborateDef :: Elaborate b m => TermDef InputAnn -> m (TermDef Ann) Source #

Elaborate a TermDef

elaborateTermDef :: Elaborate b m => TermDef InputAnn -> m (ElabInfo (TermDef Ann)) Source #

Elaborate a term definition helper function

elaborateBlock :: Elaborate b m => Block InputAnn -> m (Type, Block Ann) Source #

Elaborate a list of statements. Returns the type of the final statement as well.

elaborateStmt :: Elaborate b m => Statement InputAnn -> m (ElabInfo (Statement Ann)) Source #

Elaborate a single statement.

elaborateExpr :: Elaborate b m => InputAnn -> Expr InputAnn -> m (Expr Ann) Source #

Elaborate an expression. Traverses the expression Top-Down.

elaboratePatterns :: Elaborate b m => InputAnn -> Type -> Type -> [(Pattern, Expr InputAnn)] -> m [(Pattern, Expr Ann)] Source #

Elaborate patterns in case expressions

elaboratePattern :: Elaborate b m => InputAnn -> TypeVar -> Pattern -> m [(Var, Type)] Source #

Elaborate a single pattern match

getLitType :: Lit -> Type Source #

The type of a literal

type Solve b m = (MonadBase b m, MonadError TypeErrorA m, MonadState ElabState m, MonadReader (ElabEnv b) m) Source #

instantiate :: Solve b m => Text -> [TypeVar] -> Type -> m Type Source #

Create an instance of a type. (The type serves as a template for specialized types)

Let polymorphism gives us the ability to use a generic function in more contexts.

For example, id is a function that can work for x of any type. But our algorithm collects constraints globally, including that:

id = x -> x

one = id 1          -- constrain that the type of id is equal to the type [Int] -> tN

hello = id "hello"  -- constrain that the type of id is equal to the type [String] -> tM

We need to invent a new constraint that will define the relationship between the type of id and the arguments passing to it as an Instance of relationship.

InstanceOf t1 t2 relationship means that t1 is an instantiation of t2 (or a special case if you will). What we'll do is copy the type of t2, generate new type variables in place of all type variables inside of it, and then say that this new type t3 has an equality relationship with t1.

It's important to solve the equality constraints for each function before solving the InstanceOf constraints, so that when we instantiate we already have the final type of the function.

We will highjack the Ord instance deriving (constructors defined later are bigger) and the fact that Set is ordered to accomplish that.