This repository was archived by the owner on May 20, 2018. It is now read-only.

[WIP] Typechecking#4

Open

robrix wants to merge 109 commits intomasterfrom

Commits on Jan 10, 2016

Move unification into its own section.
Rob Rix
committed
Stub in a heading for typechecking.
Rob Rix
committed
Add a type synonym for contexts.
Rob Rix
committed
Add a type synonym for inferers.
Rob Rix
committed
Add a type synonym for checkers.
Rob Rix
committed
Remove the Inferer/Checker synonyms.
Rob Rix
committed
Add an Error case to Unification.
Rob Rix
committed
Errors don’t have a unified term.
Rob Rix
committed
Errors can equate.
Rob Rix
committed
Errors can be shown.
Rob Rix
committed
Stub in typechecking.
Rob Rix
committed
Inference.
Rob Rix
committed
Infer the type of type.
Rob Rix
committed
Infer the types of variables.
Rob Rix
committed
Parameterize Unification by the type of conflicts.
Rob Rix
committed
Unification is a Functor.
Rob Rix
committed
Revert "Unification is a Functor."
Rob Rix
committed
Revert "Parameterize Unification by the type of conflicts."
Rob Rix
committed
Add a Roll typeclass.
Rob Rix
committed
Add a Roll instance for Term.
Rob Rix
committed
Add a Roll instance for Unification.
Rob Rix
committed
Generalize type' to Roll instances.
Rob Rix
committed
Generalize implicit to Roll instances.
Rob Rix
committed
Generalize variable to Roll instances.
Rob Rix
committed
Change the type variable to r.
Rob Rix
committed
Generalize local.
Rob Rix
committed
Generalize global.
Rob Rix
committed
Generalize apply.
Rob Rix
committed
Add a Catamorphable typeclass with an instance for Term.
Rob Rix
committed
Add an Unroll typeclass.
Rob Rix
committed
Add a `para` function w/default implementation for Unrollable types.
Rob Rix
committed
Generalize maxBoundVariable to Catamorphable terms.
Rob Rix
committed
Add an Unroll instance for Term.
Rob Rix
committed
Replace the Catamorphable instance for Term with one for Unroll.
Rob Rix
committed
Move the `para` implementation into the `Unroll` instance of `Catamorphable`.
Rob Rix
committed
Move the Catamorphable instance to the bottom.
Rob Rix
committed
Add a PartialUnroll typeclass.
Rob Rix
committed
Add a PartialUnroll instance for Unification.
Rob Rix
committed
Move the typeclasses down into their own section.
Rob Rix
committed
Use the `local` constructor for the variable.
Rob Rix
committed
`roll`.
Rob Rix
committed
Handle errors in flipUnification.
Rob Rix
committed
Annotate a bunch of term types.
Rob Rix
committed
Remove the recursion schemes heading.
Rob Rix
committed
Total Unroll instances can be lowered to PartialUnroll instances.
Rob Rix
committed
Generalize maxBoundVariable to PartialUnroll.
Rob Rix
committed
Generalize lambda to Roll/PartialUnroll r.
Rob Rix
committed
Generalize --> to Roll/PartialUnroll.
Rob Rix
committed
Add an explicit instance of PartialUnroll for Term.
Rob Rix
committed
Generalize substitution to Roll/PartialUnroll.
Rob Rix
committed
Infer the types of lambdas.
Rob Rix
committed
Use the constructors for unifying variables and applications.
Rob Rix
committed
Generalize renaming to Roll/PartialUnroll.
Rob Rix
committed

Commits on Jan 11, 2016

Stub in unification of arbitrary lambdas.
Rob Rix
committed
Arbitrary lambda unification subsumes no-renaming unification.
Rob Rix
committed
Define freeVariables with a lambda expression.
Rob Rix
committed
Add a function to increment a name.
Rob Rix
committed
Add a function to compute a fresh name given some predicate.
Rob Rix
committed
Add a function to compute a fresh name given a set of names.
Rob Rix
committed
Pick a sensible fresh name given a set of names.
Rob Rix
committed
Generalize renaming to Names.
Rob Rix
committed
Select a fresh name.
Rob Rix
committed
Test that shadowed variables are not renamed.
Rob Rix
committed
Test that prime is injective.
Rob Rix
committed
Test that renaming is injective.
Rob Rix
committed
Generalize the test of renaming with shadowed variables to arbitrary bodies.
Rob Rix
committed
Factor out the priming.
Rob Rix
committed
Reconstruct the expected term from Unifications.
Rob Rix
committed
Reconstruct the actual term from Unifications.
Rob Rix
committed
Stub in a test helper for replacing terms deeply.
Rob Rix
committed
Test that the expected term is recoverable.
Rob Rix
committed
Test that the actual term is recoverable.
Rob Rix
committed
Section header for naming.
Rob Rix
committed
Alpha equivalence.
Rob Rix
committed
Test recovery of expected/actual terms up to renaming.
Rob Rix
committed
Test actual/expected terms by replacing.
Rob Rix
committed
Test that identical terms are alpha-equivalent.
Rob Rix
committed
Test that free variables are alpha-equivalent.
Rob Rix
committed
Variables are alpha equivalent.
Rob Rix
committed
Generate lambdas more often.
Rob Rix
committed
Fix a test name.
Rob Rix
committed
Unify free variables.
Rob Rix
committed
Unify lambdas up to renaming.
Rob Rix
committed
Alpha-equivalence is defined up to renaming.
Rob Rix
committed
Remove some unused terms.
Rob Rix
committed

Commits on Jan 12, 2016

As an experiment, represent errors with conflicts.
Rob Rix
committed
Remove the Error case from Unification.
Rob Rix
committed
Typecheck applications in suspension.
Rob Rix
committed
Typecheck applications of functions in suspension.
Rob Rix
committed
Stub in an applySubstitution function.
Rob Rix
committed
Substitute inside lambdas.
Rob Rix
committed
Remove overlapped patterns.
Rob Rix
committed
Substitute in application types.
Rob Rix
committed
Test the equivalence of checking against implicit & inference.
Rob Rix
committed
Check lambda types against Type, rather than unifying against it.
Rob Rix
committed
Test that free variables do not typecheck.
Rob Rix
committed
Test the inference of bound variables.
Rob Rix
committed
Test that inferred types are checked.
Rob Rix
committed
Test the inference of simple function types.
Rob Rix
committed
Simplify the test of simple function type inference.
Rob Rix
committed
Typecheck the bodies of lambdas.
Rob Rix
committed
Add another test of simple function type inference.
Rob Rix
committed
Test the inference of `identity`’s type.
Rob Rix
committed
Test the inference of `constant`’s type.
Rob Rix
committed
Use the parameter type, and not its type, as the domain.
Rob Rix
committed
Shadow >> infix.
Rob Rix
committed
Check lambdas against types.
Rob Rix
committed
Make the >> definition available to all cases.
Rob Rix
committed
Strip some leading indentation.
Rob Rix
committed