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