giml-language-0.1.0.0: A purely functional programming language with emphasis on structural typing
Safe HaskellSafe-Inferred
LanguageGHC2021

Language.Giml.Types.Infer.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

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

data ElabEnv b Source #

The environment we use.

Constructors

ElabEnv 

Fields

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-language-0.1.0.0-D00xD3NNyCIERJGkwuGtlB" '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

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

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

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.