Hydra.Inference.AlgorithmWBridge

Wrapper for @wisnesky's Algorithm W implementation which makes it into an alternative inferencer for Hydra

Documentation

data HydraContext

Constructors

HydraContext (Map Name Primitive)

boundTypeVariablesInSystemFTerm :: Term -> [Name]

Find all of the bound variables in the type annotations within a System F term. This function considers the types in "typed terms" (term:type), domain types on lambdas (v:type.term), and also type abstractions (/v.term) to provide bound type variables.

boundTypeVariablesInTermOrdered :: Term -> [Name]

boundVariablesInTypeOrdered :: Type -> [Name]

Finds all of the universal type variables in a type expression, in the order in which they appear. Note: this function assumes that there are no shadowed type variables, as in (forall a. forall a. a) TODO: redundant with variablesInTypeOrdered

normalizeBoundTypeVariablesInSystemFTerm :: Term -> Term

Replace arbitrary bound type variables like v, a, v_12 with the systematic type variables t0, t1, t2, ... following a canonical ordering in the term. This function assumes that the bound variables do not also appear free in the type expressions of the term, which in Hydra is made less likely by using the unusual naming convention tv_0, tv_1, etc. for temporary variables.

replaceTypeVariables :: Map Name Name -> Type -> Type

replaceTypeVariablesInSystemFTerm :: Map Name Name -> Term -> Term

variablesInTypeOrdered :: Bool -> Type -> [Name]

Find the variables (both bound and free) in a type expression, following a preorder traversal of the expression.

hydraTermToStlc :: HydraContext -> Term -> Either String Expr

hydraTypeSchemeToStlc :: TypeScheme -> Either String TypSch

systemFExprToHydra :: FExpr -> Either String Term

systemFTypeToHydra :: FTy -> Either String TypeScheme

inferWithAlgorithmW :: HydraContext -> Term -> IO Term

inferExpr :: Expr -> IO (FExpr, FTy)