giml-language-0.1.0.0: A purely functional programming language with emphasis on structural typing
Safe HaskellNone
LanguageHaskell2010

Language.Giml.Types.Infer

Description

Type inference

Our type inference algorithm works in stages:

First, we elaborate the AST and collect constraints. Then, we solve these constraints and get back a substitution. We go over the AST again, replacing the type variables we added in the elaboration stage with concrete types.

The constraints of each group of definitions are solved separately and in order.

Synopsis

Run

infer :: File InputAnn -> Either TypeErrorA (File Ann) Source #

Infer the types for all expressions in a source file

Types

type InputAnn = Ann Source #

The annotation of the input

data Ann Source #

The annotation of the output: the input + the type

Constructors

Ann 

Fields

Instances

Instances details
Eq Ann Source # 
Instance details

Defined in Language.Giml.Types.Infer

Methods

(==) :: Ann -> Ann -> Bool #

(/=) :: Ann -> Ann -> Bool #

Data Ann Source # 
Instance details

Defined in Language.Giml.Types.Infer

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Ann -> c Ann #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Ann #

toConstr :: Ann -> Constr #

dataTypeOf :: Ann -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Ann) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Ann) #

gmapT :: (forall b. Data b => b -> b) -> Ann -> Ann #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ann -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ann -> r #

gmapQ :: (forall d. Data d => d -> u) -> Ann -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Ann -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Ann -> m Ann #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Ann -> m Ann #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Ann -> m Ann #

Ord Ann Source # 
Instance details

Defined in Language.Giml.Types.Infer

Methods

compare :: Ann -> Ann -> Ordering #

(<) :: Ann -> Ann -> Bool #

(<=) :: Ann -> Ann -> Bool #

(>) :: Ann -> Ann -> Bool #

(>=) :: Ann -> Ann -> Bool #

max :: Ann -> Ann -> Ann #

min :: Ann -> Ann -> Ann #

Show Ann Source # 
Instance details

Defined in Language.Giml.Types.Infer

Methods

showsPrec :: Int -> Ann -> ShowS #

show :: Ann -> String #

showList :: [Ann] -> ShowS #

Pretty Ann Source # 
Instance details

Defined in Language.Giml.Types.Infer

Methods

pretty :: Ann -> Doc ann #

prettyList :: [Ann] -> Doc ann #

data Constraint Source #

Represents the constraints on types we collect during the elaboration phase.

Constructors

Equality Type Type

The two type should be equal.

InstanceOf Type Type

The first type is an instantiation of the second (see instantiate).

Instances

Instances details
Eq Constraint Source # 
Instance details

Defined in Language.Giml.Types.Infer

Data Constraint Source # 
Instance details

Defined in Language.Giml.Types.Infer

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Constraint -> c Constraint #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Constraint #

toConstr :: Constraint -> Constr #

dataTypeOf :: Constraint -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Constraint) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Constraint) #

gmapT :: (forall b. Data b => b -> b) -> Constraint -> Constraint #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Constraint -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Constraint -> r #

gmapQ :: (forall d. Data d => d -> u) -> Constraint -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Constraint -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Constraint -> m Constraint #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Constraint -> m Constraint #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Constraint -> m Constraint #

Ord Constraint Source # 
Instance details

Defined in Language.Giml.Types.Infer

Show Constraint Source # 
Instance details

Defined in Language.Giml.Types.Infer

Pretty Constraint Source # 
Instance details

Defined in Language.Giml.Types.Infer

Methods

pretty :: Constraint -> Doc ann #

prettyList :: [Constraint] -> Doc ann #

type ConstraintA = (Constraint, InputAnn) Source #

A constraint with the input annotation.

type Constraints = Set ConstraintA Source #

A Set of constraints.

type Substitution = Map TypeVar (InputAnn, Type) Source #

A mapping from type variable to types. Also contains the source position for error reporting. This is the output of the constraint solving phase.

data Typer Source #

Used during elaboration to represent the type of names in scope.

Constructors

Monomorphic Type

This type is a monomorphic type so we can just use it.

Polymorphic TypeVar

This type represents an polymorphic type that should be instantiate later.

Instances

Instances details
Eq Typer Source # 
Instance details

Defined in Language.Giml.Types.Infer

Methods

(==) :: Typer -> Typer -> Bool #

(/=) :: Typer -> Typer -> Bool #

Data Typer Source # 
Instance details

Defined in Language.Giml.Types.Infer

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Typer -> c Typer #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Typer #

toConstr :: Typer -> Constr #

dataTypeOf :: Typer -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Typer) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Typer) #

gmapT :: (forall b. Data b => b -> b) -> Typer -> Typer #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Typer -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Typer -> r #

gmapQ :: (forall d. Data d => d -> u) -> Typer -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Typer -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Typer -> m Typer #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Typer -> m Typer #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Typer -> m Typer #

Ord Typer Source # 
Instance details

Defined in Language.Giml.Types.Infer

Methods

compare :: Typer -> Typer -> Ordering #

(<) :: Typer -> Typer -> Bool #

(<=) :: Typer -> Typer -> Bool #

(>) :: Typer -> Typer -> Bool #

(>=) :: Typer -> Typer -> Bool #

max :: Typer -> Typer -> Typer #

min :: Typer -> Typer -> Typer #

Show Typer Source # 
Instance details

Defined in Language.Giml.Types.Infer

Methods

showsPrec :: Int -> Typer -> ShowS #

show :: Typer -> String #

showList :: [Typer] -> ShowS #

General Utils

throwErr :: MonadError TypeErrorA m => [InputAnn] -> TypeError -> m a Source #

Throw an error with annotation.

getType :: Expr Ann -> Type Source #

Retrieve the type of an expression. Will explode when used on a non EAnnotated node.

Elaborate

elaborate :: [Datatype ()] -> Env Type -> File InputAnn -> Either TypeErrorA (File Ann, ElabState) Source #

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: AST
  • Output: Annotated AST with types (to the best of our abilities) + constraints on those types

Types

type Env a = Map Var a Source #

An environment from a name to something.

type VariantEnv a = Map Constr (VariantSig a) Source #

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

data VariantSig a Source #

Relevant information about a data constructor.

Constructors

VariantSig 

Instances

Instances details
Eq a => Eq (VariantSig a) Source # 
Instance details

Defined in Language.Giml.Types.Infer

Methods

(==) :: VariantSig a -> VariantSig a -> Bool #

(/=) :: VariantSig a -> VariantSig a -> Bool #

Data a => Data (VariantSig a) Source # 
Instance details

Defined in Language.Giml.Types.Infer

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> VariantSig a -> c (VariantSig a) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (VariantSig a) #

toConstr :: VariantSig a -> Constr #

dataTypeOf :: VariantSig a -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (VariantSig a)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (VariantSig a)) #

gmapT :: (forall b. Data b => b -> b) -> VariantSig a -> VariantSig a #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> VariantSig a -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> VariantSig a -> r #

gmapQ :: (forall d. Data d => d -> u) -> VariantSig a -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> VariantSig a -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> VariantSig a -> m (VariantSig a) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> VariantSig a -> m (VariantSig a) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> VariantSig a -> m (VariantSig a) #

Ord a => Ord (VariantSig a) Source # 
Instance details

Defined in Language.Giml.Types.Infer

Show a => Show (VariantSig a) Source # 
Instance details

Defined in Language.Giml.Types.Infer

data ElabState Source #

The state we keep during elaboration.

Constructors

ElabState 

Fields

data ElabEnv Source #

The environment we use.

Constructors

ElabEnv 

Fields

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

The monadic capabilities for the elaboration phase.

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 Typer

    A definition to add to the environment for the next statements, if needed.

Utils

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

Try to find the type of a variable in scope.

lookupVar :: Elaborate m => InputAnn -> Var -> m Typer Source #

Same as lookupVarMaybe but throws an UnboundVar error on failure.

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

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

insertToEnv :: Env Typer -> ElabEnv -> ElabEnv Source #

Adding new variable into the scope

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

Remove variables from the scope

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

Run an elaboration function with extra variables in scope.

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

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

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

Run an elaboration function without some variables in scope.

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

Lookup variant in env

addVariantSigs :: Elaborate m => VariantEnv InputAnn -> m () Source #

Add a datatype information into the environment

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

Generate a new type variable.

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

Add a new constraint.

Algorithm

elaborateFile :: Elaborate m => [Datatype ()] -> File InputAnn -> m (File Ann) Source #

Elaborate a source file

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

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

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

Elaborate a TermDef

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

Elaborate a term definition helper function

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

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

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

Elaborate a single statement.

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

Elaborate an expression. Traverses the expression Top-Down.

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

Elaborate patterns in case expressions

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

Elaborate a single pattern match

getLitType :: Lit -> Type Source #

The type of a literal

Solve constraints

solve :: Int -> Constraints -> Either TypeErrorA (Substitution, Int) Source #

In this phase we go over the constraints one by one and try to unify them.

For example, if we see Equality (TypeVar "t1") (TypeCon Int), we create a mapping from t1 to Int (called a substitution) and we go over the rest of the constraints and replace t1 with Int (apply the substitution).

We also keep all the substitutions we created from the constraints (and merge them to one substitution but applying new substitution to the accumulated substitution).

If we see Equality (TypeCon Int) (TypeCon String), we throw a type error, because the two types do not match.

We keep going until there are no more constraints or until we encountered an error.

The result of the algorithm is the accumulated substitution.

Types

type Solve m = (MonadError TypeErrorA m, MonadState ElabState m) Source #

Monadic capabilities for the Solve algorithm

Algorithm

solveConstraints :: Solve m => Substitution -> [ConstraintA] -> m Substitution Source #

Recursively the constraints in order, passing the accumulated substitution.

solveConstraint :: Solve m => ConstraintA -> m ([ConstraintA], Substitution) Source #

Solve a constraint. Returns new constraints that may arise from this constraint and a substitution

instantiate :: Solve m => Text -> Type -> m (Env TypeVar, 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.

Substitute

API

substitute :: Substitute m => Data f => Substitution -> f -> m f Source #

Replaces all type variables for any data type that has an instance of Data using uniplate magic.

Note: uniplate magic = slow.

substituteConstraints :: Substitute m => Substitution -> [ConstraintA] -> m [ConstraintA] Source #

Replaces all type variables for constraints.

substituteSubs :: Substitute m => Substitution -> Substitution -> m Substitution Source #

Replaces all type variables for substitutions.

Types

type Substitute m = MonadError TypeErrorA m Source #

Monadic capabilities of Substitute

Algorithm

replaceTypeVar :: Substitute m => Substitution -> Type -> m Type Source #

Find type variables that appear in the substitution and replace them.

occursCheck :: Substitute m => TypeVar -> InputAnn -> Type -> m Type Source #

protect against infinite types

Utils

data Matches a b Source #

Constructors

OnlyLeft a 
OnlyRight a 
BothSides b 

unzipMatches :: [Matches a b] -> ([a], [a], [b]) Source #

Pretty printing

pltrace :: Pretty ann => Functor f => Show (f Text) => String -> f ann -> f ann Source #

Warning: pltrace left in code

pltraceM :: Pretty ann => Applicative m => Functor f => Show (f Text) => String -> f ann -> m () Source #

Warning: pltraceM left in code

pltraceC :: String -> Constraint -> Constraint Source #

Warning: pltraceC left in code

pltraceCs :: String -> [ConstraintA] -> [ConstraintA] Source #

Warning: pltraceCs left in code

ppAnn :: Ann -> Doc ann Source #

Orphan instances

Pretty SourcePos Source # 
Instance details

Methods

pretty :: SourcePos -> Doc ann #

prettyList :: [SourcePos] -> Doc ann #

Pretty Type Source # 
Instance details

Methods

pretty :: Type -> Doc ann #

prettyList :: [Type] -> Doc ann #