Module FlatCurry.TypeAnnotated.TypeInference

Library to annotate the expressions of a FlatCurry program with type information.

It can be used by any other Curry program which processes or transforms FlatCurry programs. The main operation to use is 

inferProg :: Prog -> IO (Either String (AProg TypeExpr))

which annotates a FlatCurry program with type information.

The type inference works in several steps:

  1. For each known function and constructor, either imported or defined in the module itself, the respective type is inserted into a type environment (type assumption).
  2. Every subexpression is annotated with a fresh type variable, whereas constructor and function names are annotated with a fresh variant of the type in the type assumption.
  3. Based on FlatCurry's type inference rules, type equations are generated for a function's rule.
  4. The resulting equations are solved using unification and the resulting substitution is applied to the function rule.
  5. The inferred types are then normalized such that for every function rule the type variables start with 0.

In addition, the function inferNewFunctions allows to infer the types of a list of functions whose type is not known before. Consequently, this disallows polymorphic recursive functions. Those functions are separated into strongly connected components before their types are inferred to allow mutually recursive function definitions.

In case of any error, the type inference quits with an error message.

IMPORTANT NOTE: The type inference is incomplete w.r.t. type classes and forall types. This need to be extended in the future!

Author: Jonas Oberschweiber, Bjoern Peemoeller, Michael Hanus

Version: December 2020

Summary of exported operations:

inferProg :: Prog -> IO (Either String (AProg TypeExpr))  Non-deterministic 
Infers the type of a whole program.
inferProgFromProgEnv :: [(String,Prog)] -> Prog -> Either String (AProg TypeExpr)  Deterministic 
Infers the type of a whole program w.r.t.
inferFunction :: Prog -> (String,String) -> IO (Either String (AFuncDecl TypeExpr))  Non-deterministic 
Infers the types of a single function specified by its qualified name.
inferNewFunctions :: Prog -> [FuncDecl] -> IO (Either String [AFuncDecl TypeExpr])  Non-deterministic 
Infers the types of a group of (possibly mutually recursive) functions.
inferExpr :: Prog -> Expr -> IO (Either String (AExpr TypeExpr))  Non-deterministic 
Infer the type of a single expression.
inferProgEnv :: Map (String,String) TypeExpr -> Prog -> Either String (AProg TypeExpr)  Deterministic 
Infers the type of a whole program.
inferFunctionEnv :: Map (String,String) TypeExpr -> Prog -> (String,String) -> Either String (AFuncDecl TypeExpr)  Deterministic 
Infers the types of a single function specified by its qualified name.
inferNewFunctionsEnv :: Map (String,String) TypeExpr -> String -> [FuncDecl] -> Either String [AFuncDecl TypeExpr]  Deterministic 
Infers the types of a group of (possibly mutually recursive) functions.
inferExprEnv :: Map (String,String) TypeExpr -> Expr -> Either String (AExpr TypeExpr)  Deterministic 
Infers the types of a single expression.
getTypeEnv :: Prog -> IO (Map (String,String) TypeExpr)  Non-deterministic 
Extract the type environment from the given Prog.
getTypeEnvFromProgEnv :: [(String,Prog)] -> Prog -> Either String (Map (String,String) TypeExpr)  Deterministic 
Extract the type environment from the given Prog by lookup in a module name -> Prog environment.

Exported datatypes:

TypeEnv

A type environment.

Type synonym: TypeEnv = Map QName TypeExpr

Exported operations:

inferProg :: Prog -> IO (Either String (AProg TypeExpr))  Non-deterministic 

Infers the type of a whole program.

Example call:
(inferProg p)
Parameters:
  • p : the Prog to infer
Returns:
the inferred program or an error

inferProgFromProgEnv :: [(String,Prog)] -> Prog -> Either String (AProg TypeExpr)  Deterministic 

Infers the type of a whole program w.r.t. a list of imported modules.

Example call:
(inferProgFromProgEnv p)
Parameters:
  • p : the Prog to infer
Returns:
the inferred program or an error

inferFunction :: Prog -> (String,String) -> IO (Either String (AFuncDecl TypeExpr))  Non-deterministic 

Infers the types of a single function specified by its qualified name.

Example call:
(inferFunction p q)
Parameters:
  • p : the Prog containing the function
  • q : the qualified name of the function
Returns:
the inferred function or an error

inferNewFunctions :: Prog -> [FuncDecl] -> IO (Either String [AFuncDecl TypeExpr])  Non-deterministic 

Infers the types of a group of (possibly mutually recursive) functions. Note that the functions are only monomorphically instantiated, i.e., polymorphic recursion is not supported. The given type may be too general, for instance a type variable only, and will be specialised to the inferred type.

inferExpr :: Prog -> Expr -> IO (Either String (AExpr TypeExpr))  Non-deterministic 

Infer the type of a single expression.

Example call:
(inferExpr p e)
Parameters:
  • p : the Prog containing the function
  • e : the expression
Returns:
the inferred expression or an error

inferProgEnv :: Map (String,String) TypeExpr -> Prog -> Either String (AProg TypeExpr)  Deterministic 

Infers the type of a whole program. Uses the given type environment instead of generating a new one.

Example call:
(inferProgEnv te p)
Parameters:
  • te : the type environment
  • p : the Prog to infer
Returns:
the inferred program or an error

inferFunctionEnv :: Map (String,String) TypeExpr -> Prog -> (String,String) -> Either String (AFuncDecl TypeExpr)  Deterministic 

Infers the types of a single function specified by its qualified name. Uses the given type environment instead of generating a new one.

Example call:
(inferFunctionEnv te p fun)
Parameters:
  • te : the type environment
  • p : the Prog containing the function
  • fun : the qualified name of the function
Returns:
the inferred function or an error

inferNewFunctionsEnv :: Map (String,String) TypeExpr -> String -> [FuncDecl] -> Either String [AFuncDecl TypeExpr]  Deterministic 

Infers the types of a group of (possibly mutually recursive) functions. Note that the functions are only monomorphically instantiated, i.e., polymorphic recursion is not supported. The given type may be too general, for instance a type variable only, and will be specialised to the inferred type.

inferExprEnv :: Map (String,String) TypeExpr -> Expr -> Either String (AExpr TypeExpr)  Deterministic 

Infers the types of a single expression. Uses the given type environment instead of generating a new one.

Example call:
(inferExprEnv te e)
Parameters:
  • te : the type environment
  • e : the expression
Returns:
the inferred expression or an error

getTypeEnv :: Prog -> IO (Map (String,String) TypeExpr)  Non-deterministic 

Extract the type environment from the given Prog.

Example call:
(getTypeEnv p)
Parameters:
  • p : the Prog
Returns:
a type environment

getTypeEnvFromProgEnv :: [(String,Prog)] -> Prog -> Either String (Map (String,String) TypeExpr)  Deterministic 

Extract the type environment from the given Prog by lookup in a module name -> Prog environment.

Example call:
(getTypeEnvFromProgEnv env p)
Parameters:
  • env : An environment mapping module names to Progs
  • p : the Prog
Returns:
a type environment