Skip to content
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
typechecking
Open

[WIP] Typechecking#4
robrix wants to merge 109 commits intomasterfrom
typechecking

Conversation

@robrix
Copy link
Copy Markdown

@robrix robrix commented Jan 11, 2016

  • Typecheck applications.
  • Test typechecking.
  • Fix the nested renaming bug.

Rob Rix added 30 commits January 10, 2016 12:50
Move unification into its own section.
c0e8134
Stub in a heading for typechecking.
78bb942
Add a type synonym for contexts.
670fe15
Add a type synonym for inferers.
a237756
Add a type synonym for checkers.
af492e6
Remove the Inferer/Checker synonyms.
2e7cd74
Add an Error case to Unification.
941e1e9
Errors don’t have a unified term.
c9ec209
Errors can equate.
8a7d3a8
Errors can be shown.
484486b
Stub in typechecking.
965b819
Inference.
4fb4753
Infer the type of type.
e7e3a33
Infer the types of variables.
a2f8931
Parameterize Unification by the type of conflicts.
56d4507 
Going to see if it can reasonably be a monad.
Unification is a Functor.
d76d4fb
Revert "Unification is a Functor."
d1fe642 
This reverts commit d76d4fb.
Revert "Parameterize Unification by the type of conflicts."
d657a6d 
This reverts commit 56d4507.
Add a Roll typeclass.
63001ed
Add a Roll instance for Term.
67bd56c
Add a Roll instance for Unification.
cd2a935
Generalize type' to Roll instances.
3a6312d
Generalize implicit to Roll instances.
e2ef41a
Generalize variable to Roll instances.
d9cac9a
Change the type variable to r.
382f4ed
Generalize local.
8418a71
Generalize global.
5f33d83
Generalize apply.
c03c36a
Add a Catamorphable typeclass with an instance for Term.
0037f1e
Add an Unroll typeclass.
71d47de
Rob Rix added 30 commits January 11, 2016 00:30
Generate lambdas more often.
0e80009
Fix a test name.
804bd99
Unify free variables.
3620273
Unify lambdas up to renaming.
d9d121b
Alpha-equivalence is defined up to renaming.
0c0d58d
Remove some unused terms.
f66ea99
As an experiment, represent errors with conflicts.
a5e5a2a
Remove the Error case from Unification.
d00104f
Typecheck applications in suspension.
bb2052a
Typecheck applications of functions in suspension.
e384d66
Stub in an applySubstitution function.
0df897a
Substitute inside lambdas.
d12d486
Remove overlapped patterns.
740901b
Substitute in application types.
9229ceb
Test the equivalence of checking against implicit & inference.
e3e85a4
Check lambda types against Type, rather than unifying against it.
ed623e6
Test that free variables do not typecheck.
2ede00c
Test the inference of bound variables.
912e8a7
Test that inferred types are checked.
19b097a
Test the inference of simple function types.
0d0358c
Simplify the test of simple function type inference.
57ad2a5
Typecheck the bodies of lambdas.
7c70635
Add another test of simple function type inference.
b3ed734
Test the inference of identity’s type.
0e8a928
Test the inference of constant’s type.
5ff72a4
Use the parameter type, and not its type, as the domain.
4bb7cc4
Shadow >> infix.
318fea5
Check lambdas against types.
90d1f24
Make the >> definition available to all cases.
180c8fe
Strip some leading indentation.
c3bb9be
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@robrix