Safe Haskell	None
Language	Haskell2010

FreeC.LiftedIR.Converter.Type

Contents

Translations

Description

Implements the IR to lifted IR translation, which applies the monadic lifting as described by Abel et al. in "Verifying Haskell Programs Using Constructive Type Theory".

Synopsis

liftFuncArgTypes :: Maybe Int -> [VarPat] -> Converter [Type]
liftConArgType :: QName -> Type -> Converter Type
liftVarPatType :: VarPat -> Converter (Maybe Type)
liftType :: Type -> Converter Type
liftType' :: Type -> Converter Type

Documentation

liftFuncArgTypes Source #

Arguments

:: Maybe Int	Index of the decreasing argument for recursive functions.
-> [VarPat]	The argument types.
-> Converter [Type]

Converts the argument types of a function.

liftConArgType :: QName -> Type -> Converter Type Source #

Converts a constructor argument using convertType.

All occurrences of the constructed type are marked as structurally smaller.

liftVarPatType :: VarPat -> Converter (Maybe Type) Source #

Lifts the type of an VarPat. If the argument is strict the type itself isn't lifted into the Free monad.

Translations

liftType :: Type -> Converter Type Source #

Converts a type from IR to lifted IR by lifting it into the Free monad.

This corresponds to the dagger translation for monotypes as described by Abel et al.

τ' = Free τ*

liftType' :: Type -> Converter Type Source #

Lifts a type from IR to lifted IR by adding the free arguments to constructors and lifting function types in the Free monad.

This corresponds to the star translation for monotypes as described by Abel et al.