typerbole-0.0.0.5: A typeystems library with exaggerated claims

Calculi.Lambda

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

 Source # Methodsbimap :: (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 # Source # Methodsbitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> LambdaTerm c0 a b -> f (LambdaTerm c0 c d) # Source # Methodsbifold :: 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 Typestype TypingContext (LambdaTerm c v :: * -> *) (SimplyTyped m) :: * Source #type TypeError (LambdaTerm c v :: * -> *) (SimplyTyped m) :: * Source # Methodstypecheck :: 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 Typestype TypingContext (LambdaTerm c v :: * -> *) (SystemF m p) :: * Source #type TypeError (LambdaTerm c v :: * -> *) (SystemF m p) :: * Source # Methodstypecheck :: 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 # Methodsgfoldl :: (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 # Methodscompare :: 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 # MethodsshowsPrec :: 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 # Methodsarbitrary :: 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))

## 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 # Methodscompare :: 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 # MethodsshowsPrec :: 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 #

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.