Calculi.Lambda

Typed Lambda Calculus AST.

data LambdaTerm c v t

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)

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)

Methods

bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> LambdaTerm c0 a b -> f (LambdaTerm c0 c d)

Bifoldable (LambdaTerm c0)

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)

Associated Types

type TypingContext (LambdaTerm c v :: * -> *) (SimplyTyped m) :: *

type TypeError (LambdaTerm c v :: * -> *) (SimplyTyped m) :: *

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)

(Ord c, Ord v, Ord m, Ord p) => Typecheckable (LambdaTerm c v) (SystemF m p)

Associated Types

type TypingContext (LambdaTerm c v :: * -> *) (SystemF m p) :: *

type TypeError (LambdaTerm c v :: * -> *) (SystemF m p) :: *

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)

(Eq c, Eq v, Eq t) => Eq (LambdaTerm c v t)

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)

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)

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)

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)

Methods

arbitrary :: Gen (LambdaTerm c v t)

shrink :: LambdaTerm c v t -> [LambdaTerm c v t]

type TypingContext (LambdaTerm c v) (SimplyTyped m)

type TypingContext (LambdaTerm c v) (SimplyTyped m) = SimpleTypingContext c v (SimplyTyped m)

type TypeError (LambdaTerm c v) (SimplyTyped m)

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)

type TypingContext (LambdaTerm c v) (SystemF m p) = SystemFContext c v (SystemF m p) p

type TypeError (LambdaTerm c v) (SystemF m p)

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 ()

Analysis Helpers

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

Find all the unbound variables in an expression.

Name-related errors

data NotKnownErr c v t

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)

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)

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)

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)

unlet

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) ()

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) ())

letsDependency but also return the internally used NodeMap.