-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | A lambda calculus interpreter -- -- A simple implementation of the Untyped Lambda Calculus @package lambda-calculator @version 3.1.1.0 module Language.Lambda.Shared.Errors data LambdaException -- | An expression that cannot be parsed Examples: -- -- x y = y ParseError :: Text -> LambdaException -- | A let binding nested in another expression Examples: -- -- x. let y = z x (let y = z) InvalidLet :: Text -> LambdaException -- | The expected type does not match the actual type Examples: -- -- (x: X. x) (y:Y) (x: T. x) [U] TyMismatchError :: Text -> LambdaException -- | A catch-all error that indicates a bug in this project ImpossibleError :: LambdaException -- | Returns true if the passed in value is a LamdbaExpression. Can be -- used, for example, as a shouldThrow matcher isLambdaException :: LambdaException -> Bool isLetError :: LambdaException -> Bool isParseError :: LambdaException -> Bool isImpossibleError :: LambdaException -> Bool isTyMismatchError :: LambdaException -> Bool instance GHC.Classes.Eq Language.Lambda.Shared.Errors.LambdaException instance GHC.Exception.Type.Exception Language.Lambda.Shared.Errors.LambdaException instance RIO.Prelude.Display.Display Language.Lambda.Shared.Errors.LambdaException instance GHC.Show.Show Language.Lambda.Shared.Errors.LambdaException module Language.Lambda.Shared.UniqueSupply type Unique = Text defaultUniques :: [Unique] defaultTyUniques :: [Unique] next :: (Ord name, MonadError LambdaException m) => [name] -> [name] -> m name module Language.Lambda.SystemF.Expression data SystemFExpr name -- | A global binding: `let x = y` Let :: name -> SystemFExpr name -> SystemFExpr name -- | Variable: x Var :: name -> SystemFExpr name -- | Variable annotated with type: `x:T` VarAnn :: name -> Ty name -> SystemFExpr name -- | Function application: `x y` App :: SystemFExpr name -> SystemFExpr name -> SystemFExpr name -- | Lambda abstraction: `x: X. x` Abs :: name -> Ty name -> SystemFExpr name -> SystemFExpr name -- | Type Abstraction: `X. body` TyAbs :: name -> SystemFExpr name -> SystemFExpr name -- | Type Application: `x [X]` TyApp :: SystemFExpr name -> Ty name -> SystemFExpr name data TypedExpr name TypedExpr :: SystemFExpr name -> Ty name -> TypedExpr name [teExpr] :: TypedExpr name -> SystemFExpr name [teTy] :: TypedExpr name -> Ty name data Ty name -- | Type variable (T) TyVar :: name -> Ty name -- | Type arrow (T -> U) TyArrow :: Ty name -> Ty name -> Ty name -- | Universal type (forall T. X) TyForAll :: name -> Ty name -> Ty name _expr :: Lens' (TypedExpr name) (SystemFExpr name) _ty :: Lens' (TypedExpr name) (Ty name) prettyPrint :: Pretty pretty => pretty -> Text substituteTy :: Eq name => Ty name -> name -> Ty name -> Ty name upperLambda :: Char instance GHC.Show.Show name => GHC.Show.Show (Language.Lambda.SystemF.Expression.Ty name) instance GHC.Show.Show name => GHC.Show.Show (Language.Lambda.SystemF.Expression.SystemFExpr name) instance GHC.Classes.Eq name => GHC.Classes.Eq (Language.Lambda.SystemF.Expression.SystemFExpr name) instance GHC.Show.Show name => GHC.Show.Show (Language.Lambda.SystemF.Expression.TypedExpr name) instance GHC.Classes.Eq name => GHC.Classes.Eq (Language.Lambda.SystemF.Expression.TypedExpr name) instance Prettyprinter.Internal.Pretty name => Prettyprinter.Internal.Pretty (Language.Lambda.SystemF.Expression.TypedExpr name) instance Prettyprinter.Internal.Pretty name => Prettyprinter.Internal.Pretty (Language.Lambda.SystemF.Expression.SystemFExpr name) instance Prettyprinter.Internal.Pretty name => Prettyprinter.Internal.Pretty (Language.Lambda.SystemF.Expression.Ty name) instance GHC.Classes.Eq name => GHC.Classes.Eq (Language.Lambda.SystemF.Expression.Ty name) module Language.Lambda.SystemF.Parser parseExpr :: Text -> Either ParseError (SystemFExpr Text) parseType :: Text -> Either ParseError (Ty Text) module Language.Lambda.SystemF.State data TypecheckState name TypecheckState :: Globals name -> [name] -> [name] -> TypecheckState name [tsGlobals] :: TypecheckState name -> Globals name -- | A unique supply of term-level variables [tsVarUniques] :: TypecheckState name -> [name] -- | A unique supply of type-level variables [tsTyUniques] :: TypecheckState name -> [name] type Typecheck name = StateT (TypecheckState name) (Except LambdaException) type Context name = Map name (Binding name) data Binding name BindTerm :: Ty name -> Binding name BindTy :: Binding name type Globals name = Map name (TypedExpr name) runTypecheck :: Typecheck name result -> TypecheckState name -> Either LambdaException (result, TypecheckState name) execTypecheck :: Typecheck name result -> TypecheckState name -> Either LambdaException result unsafeRunTypecheck :: Typecheck name result -> TypecheckState name -> (result, TypecheckState name) unsafeExecTypecheck :: Typecheck name result -> TypecheckState name -> result mkTypecheckState :: [name] -> [name] -> TypecheckState name _context :: SimpleGetter (TypecheckState name) (Context name) _globals :: Lens' (TypecheckState name) (Globals name) _varUniques :: Lens' (TypecheckState name) [name] _tyUniques :: Lens' (TypecheckState name) [name] getContext :: Typecheck name (Context name) getGlobals :: Typecheck name (Globals name) getVarUniques :: Typecheck name [name] getTyUniques :: Typecheck name [name] modifyGlobals :: (Globals name -> Globals name) -> Typecheck name () modifyVarUniques :: ([name] -> [name]) -> Typecheck name () modifyTyUniques :: ([name] -> [name]) -> Typecheck name () setGlobals :: Globals name -> Typecheck name () setVarUniques :: [name] -> Typecheck name () setTyUniques :: [name] -> Typecheck name () instance GHC.Show.Show name => GHC.Show.Show (Language.Lambda.SystemF.State.TypecheckState name) instance GHC.Classes.Eq name => GHC.Classes.Eq (Language.Lambda.SystemF.State.TypecheckState name) instance GHC.Show.Show name => GHC.Show.Show (Language.Lambda.SystemF.State.Binding name) instance GHC.Classes.Eq name => GHC.Classes.Eq (Language.Lambda.SystemF.State.Binding name) module Language.Lambda.SystemF.Eval -- | Evaluates an expression evalExpr :: (Pretty name, Ord name) => SystemFExpr name -> Typecheck name (SystemFExpr name) subGlobals :: Ord name => SystemFExpr name -> Typecheck name (SystemFExpr name) betaReduce :: (Ord name, Pretty name) => SystemFExpr name -> SystemFExpr name -> Typecheck name (SystemFExpr name) alphaConvert :: (Ord name, Pretty name) => [name] -> SystemFExpr name -> Typecheck name (SystemFExpr name) etaConvert :: Ord name => SystemFExpr name -> SystemFExpr name freeVarsOf :: (Ord name, Pretty name) => SystemFExpr name -> [name] module Language.Lambda.SystemF.TypeCheck type UniqueSupply n = [n] type Context' n t = Map n t typecheck :: (Ord name, Pretty name) => SystemFExpr name -> Typecheck name (Ty name) typecheckTopLevel :: (Ord name, Pretty name) => Context name -> SystemFExpr name -> Typecheck name (Ty name) typecheckLet :: (Pretty name, Ord name) => Context name -> name -> SystemFExpr name -> Typecheck name (Ty name) typecheckExpr :: (Ord name, Pretty name) => Context name -> SystemFExpr name -> Typecheck name (Ty name) typecheckVar :: Ord name => Context name -> name -> Typecheck name (Ty name) typecheckVarAnn :: (Ord name, Pretty name) => Context name -> name -> Ty name -> Typecheck name (Ty name) typecheckAbs :: (Ord name, Pretty name) => Context name -> name -> Ty name -> SystemFExpr name -> Typecheck name (Ty name) typecheckApp :: (Ord name, Pretty name) => Context name -> SystemFExpr name -> SystemFExpr name -> Typecheck name (Ty name) typecheckTyAbs :: (Ord name, Pretty name) => Context name -> name -> SystemFExpr name -> Typecheck name (Ty name) typecheckTyApp :: (Ord name, Pretty name) => Context name -> SystemFExpr name -> Ty name -> Typecheck name (Ty name) typecheckVar' :: Ord name => Context name -> name -> Maybe (Ty name) liftForAlls :: Ty name -> Ty name liftForAlls' :: Ty name -> ([name], Ty name) isTyEquivalent :: Ord name => Ty name -> Ty name -> Bool areForAllsEquivalent :: Ord name => (name, Ty name) -> (name, Ty name) -> Bool tyUnique :: Typecheck name name tyMismatchError :: Pretty ty => ty -> ty -> LambdaException tyAppMismatchError :: (Ord name, Pretty name) => Context name -> SystemFExpr name -> Ty name -> Typecheck name LambdaException module Language.Lambda.SystemF evalText :: Text -> Typecheck Text (TypedExpr Text) typecheckText :: Text -> Typecheck Text (Ty Text) runEvalText :: Text -> Globals Text -> Either LambdaException (TypedExpr Text, TypecheckState Text) runTypecheckText :: Text -> Globals Text -> Either LambdaException (Ty Text, TypecheckState Text) execEvalText :: Text -> Globals Text -> Either LambdaException (TypedExpr Text) execTypecheckText :: Text -> Globals Text -> Either LambdaException (Ty Text) unsafeExecEvalText :: Text -> Globals Text -> TypedExpr Text unsafeExecTypecheckText :: Text -> Globals Text -> Ty Text defaultUniques :: [Unique] defaultTyUniques :: [Unique] mkState :: Globals Text -> TypecheckState Text module Language.Lambda.Untyped.Expression data LambdaExpr name -- | Variables Var :: name -> LambdaExpr name -- | Application App :: LambdaExpr name -> LambdaExpr name -> LambdaExpr name -- | Abstractions Abs :: name -> LambdaExpr name -> LambdaExpr name -- | Let bindings Let :: name -> LambdaExpr name -> LambdaExpr name lambda :: Char prettyPrint :: Pretty name => LambdaExpr name -> Text instance GHC.Show.Show name => GHC.Show.Show (Language.Lambda.Untyped.Expression.LambdaExpr name) instance GHC.Classes.Eq name => GHC.Classes.Eq (Language.Lambda.Untyped.Expression.LambdaExpr name) instance Prettyprinter.Internal.Pretty name => Prettyprinter.Internal.Pretty (Language.Lambda.Untyped.Expression.LambdaExpr name) module Language.Lambda.Untyped.Parser parseExpr :: Text -> Either ParseError (LambdaExpr Text) module Language.Lambda.Untyped.State -- | The evaluation state data EvalState name EvalState :: Globals name -> [name] -> EvalState name [esGlobals] :: EvalState name -> Globals name -- | Unused unique names [esUniques] :: EvalState name -> [name] -- | A stateful computation type Eval name = StateT (EvalState name) (Except LambdaException) -- | A mapping of global variables to expressions type Globals name = Map name (LambdaExpr name) -- | Run an evalualation runEval :: Eval name result -> EvalState name -> Either LambdaException (result, EvalState name) -- | Run an evalualation, throwing away the final state execEval :: Eval name result -> EvalState name -> Either LambdaException result -- | Run an evaluation, throwing away the final state. If the result is an -- error, throws it unsafeExecEval :: Eval name result -> EvalState name -> result -- | Run an evaluation. If the result is an error, throws it unsafeRunEval :: Eval name result -> EvalState name -> (result, EvalState name) globals :: Lens' (EvalState name) (Globals name) uniques :: Lens' (EvalState name) [name] -- | Create an EvalState mkEvalState :: [name] -> EvalState name -- | Access globals from the state monad getGlobals :: Eval name (Globals name) -- | Access unique supply from state monad getUniques :: Eval name [name] setGlobals :: Globals name -> Eval name () setUniques :: [name] -> Eval name () module Language.Lambda.Untyped.Eval -- | The evaluation state data EvalState name EvalState :: Globals name -> [name] -> EvalState name [esGlobals] :: EvalState name -> Globals name -- | Unused unique names [esUniques] :: EvalState name -> [name] -- | Evaluate an expression evalExpr :: (Pretty name, Ord name) => LambdaExpr name -> Eval name (LambdaExpr name) -- | Look up free vars that have global bindings and substitute them subGlobals :: Ord name => Map name (LambdaExpr name) -> LambdaExpr name -> LambdaExpr name -- | Function application betaReduce :: (Eq name, Pretty name) => LambdaExpr name -> LambdaExpr name -> Eval name (LambdaExpr name) -- | Rename abstraction parameters to avoid name captures alphaConvert :: Eq name => [name] -> LambdaExpr name -> Eval name (LambdaExpr name) -- | Eliminite superfluous abstractions etaConvert :: Eq n => LambdaExpr n -> LambdaExpr n -- | Find the free variables in an expression freeVarsOf :: Eq n => LambdaExpr n -> [n] module Language.Lambda.Untyped evalText :: Text -> Eval Text (LambdaExpr Text) runEvalText :: Text -> Globals Text -> Either LambdaException (LambdaExpr Text, EvalState Text) execEvalText :: Text -> Globals Text -> Either LambdaException (LambdaExpr Text) unsafeExecEvalText :: Text -> Globals Text -> LambdaExpr Text defaultUniques :: [Unique]