Safe Haskell	None
Language	Haskell2010

Calculi.Lambda

Contents

Typed Lambda Calculus AST.
- Analysis Helpers
- Name-related errors
Let declaration helpers

Synopsis

Typed Lambda Calculus AST.

data LambdaTerm c v t Source #

A simple, typed lambda calculus AST with constants.

Constructors

Variable v	A reference to a variable.
Constant c	A constant value, such as literals or constructors.
Apply (LambdaTerm c v t) (LambdaTerm c v t)	An application of one expression to another.
Lambda (v, t) (LambdaTerm c v t)	A lambda expression, with a variable definition and a function body.

Instances

Bifunctor (LambdaTerm c0) Source #
Methods bimap :: (a -> b) -> (c -> d) -> LambdaTerm c0 a c -> LambdaTerm c0 b d # first :: (a -> b) -> LambdaTerm c0 a c -> LambdaTerm c0 b c # second :: (b -> c) -> LambdaTerm c0 a b -> LambdaTerm c0 a c #
Bitraversable (LambdaTerm c0) Source #
Methods bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> LambdaTerm c0 a b -> f (LambdaTerm c0 c d) #
Bifoldable (LambdaTerm c0) Source #
Methods bifold :: Monoid m => LambdaTerm c0 m m -> m # bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> LambdaTerm c0 a b -> m # bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> LambdaTerm c0 a b -> c # bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> LambdaTerm c0 a b -> c #
(Ord m, Ord c, Ord v) => Typecheckable (LambdaTerm c v) (SimplyTyped m) Source #
Associated Types type TypingContext (LambdaTerm c v :: * -> ) (SimplyTyped m) :: Source # type TypeError (LambdaTerm c v :: * -> ) (SimplyTyped m) :: Source # Methods typecheck :: TypingContext (LambdaTerm c v) (SimplyTyped m) -> LambdaTerm c v (SimplyTyped m) -> Either [TypeError (LambdaTerm c v) (SimplyTyped m)] (TypingContext (LambdaTerm c v) (SimplyTyped m), SimplyTyped m) Source #
(Ord c, Ord v, Ord m, Ord p) => Typecheckable (LambdaTerm c v) (SystemF m p) Source #
Associated Types type TypingContext (LambdaTerm c v :: * -> ) (SystemF m p) :: Source # type TypeError (LambdaTerm c v :: * -> ) (SystemF m p) :: Source # Methods typecheck :: TypingContext (LambdaTerm c v) (SystemF m p) -> LambdaTerm c v (SystemF m p) -> Either [TypeError (LambdaTerm c v) (SystemF m p)] (TypingContext (LambdaTerm c v) (SystemF m p), SystemF m p) Source #
(Eq c, Eq v, Eq t) => Eq (LambdaTerm c v t) Source #
Methods (==) :: LambdaTerm c v t -> LambdaTerm c v t -> Bool # (/=) :: LambdaTerm c v t -> LambdaTerm c v t -> Bool #
(Data c, Data v, Data t) => Data (LambdaTerm c v t) Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LambdaTerm c v t -> c (LambdaTerm c v t) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (LambdaTerm c v t) # toConstr :: LambdaTerm c v t -> Constr # dataTypeOf :: LambdaTerm c v t -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c (LambdaTerm c v t)) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (LambdaTerm c v t)) # gmapT :: (forall b. Data b => b -> b) -> LambdaTerm c v t -> LambdaTerm c v t # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LambdaTerm c v t -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LambdaTerm c v t -> r # gmapQ :: (forall d. Data d => d -> u) -> LambdaTerm c v t -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> LambdaTerm c v t -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> LambdaTerm c v t -> m (LambdaTerm c v t) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LambdaTerm c v t -> m (LambdaTerm c v t) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LambdaTerm c v t -> m (LambdaTerm c v t) #
(Ord c, Ord v, Ord t) => Ord (LambdaTerm c v t) Source #
Methods compare :: LambdaTerm c v t -> LambdaTerm c v t -> Ordering # (<) :: LambdaTerm c v t -> LambdaTerm c v t -> Bool # (<=) :: LambdaTerm c v t -> LambdaTerm c v t -> Bool # (>) :: LambdaTerm c v t -> LambdaTerm c v t -> Bool # (>=) :: LambdaTerm c v t -> LambdaTerm c v t -> Bool # max :: LambdaTerm c v t -> LambdaTerm c v t -> LambdaTerm c v t # min :: LambdaTerm c v t -> LambdaTerm c v t -> LambdaTerm c v t #
(Show c, Show v, Show t) => Show (LambdaTerm c v t) Source #
Methods showsPrec :: Int -> LambdaTerm c v t -> ShowS # show :: LambdaTerm c v t -> String # showList :: [LambdaTerm c v t] -> ShowS #
(Arbitrary c, Data c, Arbitrary v, Data v, Arbitrary t, Data t) => Arbitrary (LambdaTerm c v t) Source #
Methods arbitrary :: Gen (LambdaTerm c v t) # shrink :: LambdaTerm c v t -> [LambdaTerm c v t] #
type TypingContext (LambdaTerm c v) (SimplyTyped m) Source #
type TypingContext (LambdaTerm c v) (SimplyTyped m) = SimpleTypingContext c v (SimplyTyped m)
type TypeError (LambdaTerm c v) (SimplyTyped m) Source #
type TypeError (LambdaTerm c v) (SimplyTyped m) = ErrorContext' (LambdaTerm c v) (SimplyTyped m) (SimplyTypedErr c v (SimplyTyped m))
type TypingContext (LambdaTerm c v) (SystemF m p) Source #
type TypingContext (LambdaTerm c v) (SystemF m p) = SystemFContext c v (SystemF m p) p
type TypeError (LambdaTerm c v) (SystemF m p) Source #
type TypeError (LambdaTerm c v) (SystemF m p) = ErrorContext' (LambdaTerm c v) (SystemF m p) (SystemFErr c v (SystemF m p))

type UntypedLambdaExpr c v = LambdaTerm c v () Source #

Analysis Helpers

freeVars :: Ord v => LambdaTerm c v t -> Set v Source #

Find all the unbound variables in an expression.

Name-related errors

data NotKnownErr c v t Source #

Name-related errors, for when there's a variable, type or constant that doesn't appear in the environment that was given to the typechecker.

Constructors

UnknownType t	A type appears that is not in scope
UnknownVariable v	A variable appears that is not in scope
UnknownConstant c	A constant appears that is not in scope

Instances

(Eq c, Eq v, Eq t) => Eq (NotKnownErr c v t) Source #
Methods (==) :: NotKnownErr c v t -> NotKnownErr c v t -> Bool # (/=) :: NotKnownErr c v t -> NotKnownErr c v t -> Bool #
(Ord c, Ord v, Ord t) => Ord (NotKnownErr c v t) Source #
Methods compare :: NotKnownErr c v t -> NotKnownErr c v t -> Ordering # (<) :: NotKnownErr c v t -> NotKnownErr c v t -> Bool # (<=) :: NotKnownErr c v t -> NotKnownErr c v t -> Bool # (>) :: NotKnownErr c v t -> NotKnownErr c v t -> Bool # (>=) :: NotKnownErr c v t -> NotKnownErr c v t -> Bool # max :: NotKnownErr c v t -> NotKnownErr c v t -> NotKnownErr c v t # min :: NotKnownErr c v t -> NotKnownErr c v t -> NotKnownErr c v t #
(Show c, Show v, Show t) => Show (NotKnownErr c v t) Source #
Methods showsPrec :: Int -> NotKnownErr c v t -> ShowS # show :: NotKnownErr c v t -> String # showList :: [NotKnownErr c v t] -> ShowS #

Let declaration helpers

type LetDeclr c v t = ((v, t), LambdaTerm c v t) Source #

unlet Source #

Arguments

:: (Ord c, Ord v, Ord t)
=> [LetDeclr c v t]	The list of declarations in a let expression
-> LambdaTerm c v t	The body of the let declaration
-> Either [[LetDeclr c v t]] (LambdaTerm c v t)	Either a list of cyclic lets or the final expression

Unlet non-cyclic let expressions.

letsDependency :: (DynGraph gr, Ord c, Ord v, Ord t) => [LetDeclr c v t] -> gr (LetDeclr c v t) () Source #

Given the contents of a let expression's declarations, generate a graph showing the dependencies between each declaration, including recursion as loops.

letsDependency' :: forall gr c v t. (DynGraph gr, Ord c, Ord v, Ord t) => [LetDeclr c v t] -> (NodeMap (LetDeclr c v t), gr (LetDeclr c v t) ()) Source #

letsDependency but also return the internally used NodeMap.