Module FlatCurry.TypeAnnotated.TypeInference

Author

Jonas Oberschweiber, Bjoern Peemoeller, Michael Hanus

Version

November 2025

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:

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).
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.
Based on FlatCurry's type inference rules, type equations are generated for a function's rule.
The resulting equations are solved using unification and the resulting substitution is applied to the function rule.
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!

Exported Datatypes:

TypeEnv

Exported Functions:

getTypeEnv getTypeEnvFromProgEnv inferExpr inferExprEnv inferFunction inferFunctionEnv inferNewFunctions inferNewFunctionsEnv inferProg inferProgEnv inferProgFromProgEnv

Exported Datatypes

type TypeEnv
                  = Map QName TypeExpr

A type environment.

Exported Functions

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

Infers the type of a whole program.

`:: Prog`	the Prog to infer
`-> IO (Either String (AProg TypeExpr))`	the inferred program or an error

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

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

`:: [(String, Prog)]`	the Prog to infer
`-> Prog`
`-> Either String (AProg TypeExpr)`	the inferred program or an error

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

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

`:: Prog`	the Prog containing the function
`-> QName`	the qualified name of the function
`-> IO (Either String (AFuncDecl TypeExpr))`	the inferred function or an error

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

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))

Infer the type of a single expression.

`:: Prog`	the Prog containing the function
`-> Expr`	the expression
`-> IO (Either String (AExpr TypeExpr))`	the inferred expression or an error

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

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

`:: TypeEnv`	the type environment
`-> Prog`	the Prog to infer
`-> Either String (AProg TypeExpr)`	the inferred program or an error

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

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

`:: TypeEnv`	the type environment
`-> Prog`	the Prog containing the function
`-> QName`	the qualified name of the function
`-> Either String (AFuncDecl TypeExpr)`	the inferred function or an error

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

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

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

`:: TypeEnv`	the type environment
`-> Expr`	the expression
`-> Either String (AExpr TypeExpr)`	the inferred expression or an error

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

Extract the type environment from the given Prog.

`:: Prog`	the Prog
`-> IO TypeEnv`	a type environment

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

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

`:: [(String, Prog)]`	An environment mapping module names to Progs
`-> Prog`	the Prog
`-> Either String TypeEnv`	a type environment