Language.Sifflet.TypeCheck

Documentation

valueType :: Value -> SuccFail Type

Determine the type of a value. May result in a type variable.

typeCheckValues :: [String] -> [Type] -> [Value] -> SuccFail [Value]

Check whether the values agree with the types (which may be abstract)

This is *probably* too lenient in the case of type variables: it can pass a mixed-type list.

typeVarsIn :: Type -> [TypeVarName]

type Subst = TypeVarName -> Type

The type of a substitution function, which maps type variables to types

subst :: Subst -> Type -> Type

Apply a substitution function to a type (possibly a type with variables)

substComp :: Subst -> Subst -> Subst

Composing two substitutions

idSubst :: Subst

Identity substitution

deltaSubst :: TypeVarName -> Type -> Subst

A delta substitution is one that affects just a single variable.

extend :: Subst -> TypeVarName -> Type -> SuccFail Subst

Try to extend a substitution by adding a single variable-value pair

unify :: Subst -> (Type, Type) -> SuccFail Subst

data TypeScheme

A TypeScheme (TypeScheme schematicVariables typeExpression) is a sort of type template, in which schematic variables (i.e., type parameters or generics) are made explicit; any other type variables in the type expression are unknowns

Constructors

TypeScheme [TypeVarName] Type

Instances

Eq TypeScheme

Show TypeScheme

schematicsTS :: TypeScheme -> [TypeVarName]

unknownsTS :: TypeScheme -> [TypeVarName]

substTS :: Subst -> TypeScheme -> TypeScheme

Apply a substitution to a type scheme, taking care to affect only the unknowns, not the schematic variables

type TypeEnv = Map TypeVarName TypeScheme

A type environment maps type variable names to type schemes. Oh, is it really type variable names, or just names? It seems to me that in envToTypeEnv, it's function names, instead of type variable names.

emptyTypeEnv :: TypeEnv

install :: TypeEnv -> TypeVarName -> TypeScheme -> TypeEnv

Insert a new type variable and its type scheme value

unknownsTE :: TypeEnv -> [TypeVarName]

The unknowns of a type environment

substTE :: Subst -> TypeEnv -> TypeEnv

data NameSupply

A source of variable names

Constructors

NameSupply TypeVarName Int

Instances

Eq NameSupply

Show NameSupply

newNameSupply :: TypeVarName -> NameSupply

Creates a name supply

nameSupplyNext :: NameSupply -> (TypeVarName, NameSupply)

Produces next variable from a name supply

nameSupplyTake :: NameSupply -> Int -> ([TypeVarName], NameSupply)

Produces next several variables from a name supply

tcExpr :: TypeEnv -> NameSupply -> Expr -> SuccFail (Subst, Type, NameSupply)

Type check an expression

tcExprs :: TypeEnv -> NameSupply -> [Expr] -> SuccFail (Subst, [Type], NameSupply)

tcVar :: TypeEnv -> NameSupply -> String -> SuccFail (Subst, Type, NameSupply)

Type check a variable (actually the variable name). Find the type scheme associated with the variable in the type environment. Return a new instance of the type scheme, in which its schematic variables are replaced by new variables, and the unknowns are left as they are.

newInstance :: NameSupply -> TypeScheme -> (Type, NameSupply)

arrow :: Type -> Type -> Type

envToTypeEnv :: Env -> TypeEnv

Create a TypeEnv from an Env Bindings on the left replace bindings of the same name on the right, if any.

baseTypeEnv :: TypeEnv

The base type environment, derived from the base environment of the Sifflet language (built-in functions)

fromLambdaType :: Type -> SuccFail ([Type], Type)

decideTypes :: String -> Expr -> [String] -> Env -> SuccFail ([Type], Type)

Decide the type of a function -- called by the function editor when the Apply button is clicked. decideTypes tries to find the argument types and return type of an expression considered as the body of a function, at the same time checking for consistency of inputs and outputs between the parts of the expression. It returns Succ (argtypes, returntype) if successful; Fail errormessage otherwise.