Skip to content
This repository has been archived by the owner on May 20, 2018. It is now read-only.

[WIP] Typechecking #4

Open
wants to merge 109 commits into
base: master
Choose a base branch
from
Open

[WIP] Typechecking #4

Changes from 1 commit
Commits
Show all changes
109 commits
Select commit Hold shift + click to select a range
c0e8134
Move unification into its own section.
robrix Jan 10, 2016
78bb942
Stub in a heading for typechecking.
robrix Jan 10, 2016
670fe15
Add a type synonym for contexts.
robrix Jan 10, 2016
a237756
Add a type synonym for inferers.
robrix Jan 10, 2016
af492e6
Add a type synonym for checkers.
robrix Jan 10, 2016
2e7cd74
Remove the Inferer/Checker synonyms.
robrix Jan 10, 2016
941e1e9
Add an Error case to Unification.
robrix Jan 10, 2016
c9ec209
Errors don’t have a unified term.
robrix Jan 10, 2016
8a7d3a8
Errors can equate.
robrix Jan 10, 2016
484486b
Errors can be shown.
robrix Jan 10, 2016
965b819
Stub in typechecking.
robrix Jan 10, 2016
4fb4753
Inference.
robrix Jan 10, 2016
e7e3a33
Infer the type of type.
robrix Jan 10, 2016
a2f8931
Infer the types of variables.
robrix Jan 10, 2016
56d4507
Parameterize Unification by the type of conflicts.
robrix Jan 10, 2016
d76d4fb
Unification is a Functor.
robrix Jan 10, 2016
d1fe642
Revert "Unification is a Functor."
robrix Jan 10, 2016
d657a6d
Revert "Parameterize Unification by the type of conflicts."
robrix Jan 10, 2016
63001ed
Add a Roll typeclass.
robrix Jan 10, 2016
67bd56c
Add a Roll instance for Term.
robrix Jan 10, 2016
cd2a935
Add a Roll instance for Unification.
robrix Jan 10, 2016
3a6312d
Generalize type' to Roll instances.
robrix Jan 10, 2016
e2ef41a
Generalize implicit to Roll instances.
robrix Jan 10, 2016
d9cac9a
Generalize variable to Roll instances.
robrix Jan 10, 2016
382f4ed
Change the type variable to r.
robrix Jan 10, 2016
8418a71
Generalize local.
robrix Jan 10, 2016
5f33d83
Generalize global.
robrix Jan 10, 2016
c03c36a
Generalize apply.
robrix Jan 10, 2016
0037f1e
Add a Catamorphable typeclass with an instance for Term.
robrix Jan 10, 2016
71d47de
Add an Unroll typeclass.
robrix Jan 10, 2016
1037360
Add a `para` function w/default implementation for Unrollable types.
robrix Jan 10, 2016
da516ed
Generalize maxBoundVariable to Catamorphable terms.
robrix Jan 10, 2016
1622693
Add an Unroll instance for Term.
robrix Jan 10, 2016
efc1bd5
Replace the Catamorphable instance for Term with one for Unroll.
robrix Jan 10, 2016
d5e7cec
Move the `para` implementation into the `Unroll` instance of `Catamor…
robrix Jan 10, 2016
2d95bc6
Move the Catamorphable instance to the bottom.
robrix Jan 10, 2016
3658b6c
Add a PartialUnroll typeclass.
robrix Jan 10, 2016
adebe6e
Add a PartialUnroll instance for Unification.
robrix Jan 10, 2016
ae64762
Move the typeclasses down into their own section.
robrix Jan 10, 2016
466d112
Use the `local` constructor for the variable.
robrix Jan 10, 2016
d83a75c
`roll`.
robrix Jan 10, 2016
c645a1f
Handle errors in flipUnification.
robrix Jan 10, 2016
0d3f3d3
Annotate a bunch of term types.
robrix Jan 10, 2016
4d04400
Remove the recursion schemes heading.
robrix Jan 10, 2016
50140a3
Total Unroll instances can be lowered to PartialUnroll instances.
robrix Jan 10, 2016
357e957
Generalize maxBoundVariable to PartialUnroll.
robrix Jan 10, 2016
0cb5baa
Generalize lambda to Roll/PartialUnroll r.
robrix Jan 10, 2016
74ba982
Generalize --> to Roll/PartialUnroll.
robrix Jan 10, 2016
4460e60
Add an explicit instance of PartialUnroll for Term.
robrix Jan 10, 2016
e439086
Generalize substitution to Roll/PartialUnroll.
robrix Jan 10, 2016
5492dcf
Infer the types of lambdas.
robrix Jan 10, 2016
100f99e
Use the constructors for unifying variables and applications.
robrix Jan 10, 2016
cffca38
Generalize renaming to Roll/PartialUnroll.
robrix Jan 10, 2016
199dfbb
Stub in unification of arbitrary lambdas.
robrix Jan 11, 2016
86878e7
Arbitrary lambda unification subsumes no-renaming unification.
robrix Jan 11, 2016
17613a4
Define freeVariables with a lambda expression.
robrix Jan 11, 2016
83ef087
Add a function to increment a name.
robrix Jan 11, 2016
dfcd1a1
Add a function to compute a fresh name given some predicate.
robrix Jan 11, 2016
3343543
Add a function to compute a fresh name given a set of names.
robrix Jan 11, 2016
8d33b00
Pick a sensible fresh name given a set of names.
robrix Jan 11, 2016
0818975
Generalize renaming to Names.
robrix Jan 11, 2016
4b6a1f5
Select a fresh name.
robrix Jan 11, 2016
3e59da4
Test that shadowed variables are not renamed.
robrix Jan 11, 2016
f92cb88
Test that prime is injective.
robrix Jan 11, 2016
997dac9
Test that renaming is injective.
robrix Jan 11, 2016
c3de2e5
Generalize the test of renaming with shadowed variables to arbitrary …
robrix Jan 11, 2016
bbde0cc
Factor out the priming.
robrix Jan 11, 2016
cd4d342
Reconstruct the expected term from Unifications.
robrix Jan 11, 2016
36a72ca
Reconstruct the actual term from Unifications.
robrix Jan 11, 2016
5783908
Stub in a test helper for replacing terms deeply.
robrix Jan 11, 2016
e17b619
Test that the expected term is recoverable.
robrix Jan 11, 2016
4def13c
Test that the actual term is recoverable.
robrix Jan 11, 2016
7ad1a93
Section header for naming.
robrix Jan 11, 2016
5fef46e
Alpha equivalence.
robrix Jan 11, 2016
d28d51f
Test recovery of expected/actual terms up to renaming.
robrix Jan 11, 2016
21d4919
Test actual/expected terms by replacing.
robrix Jan 11, 2016
b45dd28
Test that identical terms are alpha-equivalent.
robrix Jan 11, 2016
cab0752
Test that free variables are alpha-equivalent.
robrix Jan 11, 2016
142c054
Variables are alpha equivalent.
robrix Jan 11, 2016
0e80009
Generate lambdas more often.
robrix Jan 11, 2016
804bd99
Fix a test name.
robrix Jan 11, 2016
3620273
Unify free variables.
robrix Jan 11, 2016
d9d121b
Unify lambdas up to renaming.
robrix Jan 11, 2016
0c0d58d
Alpha-equivalence is defined up to renaming.
robrix Jan 11, 2016
f66ea99
Remove some unused terms.
robrix Jan 11, 2016
a5e5a2a
As an experiment, represent errors with conflicts.
robrix Jan 12, 2016
d00104f
Remove the Error case from Unification.
robrix Jan 12, 2016
bb2052a
Typecheck applications in suspension.
robrix Jan 12, 2016
e384d66
Typecheck applications of functions in suspension.
robrix Jan 12, 2016
0df897a
Stub in an applySubstitution function.
robrix Jan 12, 2016
d12d486
Substitute inside lambdas.
robrix Jan 12, 2016
740901b
Remove overlapped patterns.
robrix Jan 12, 2016
9229ceb
Substitute in application types.
robrix Jan 12, 2016
e3e85a4
Test the equivalence of checking against implicit & inference.
robrix Jan 12, 2016
ed623e6
Check lambda types against Type, rather than unifying against it.
robrix Jan 12, 2016
2ede00c
Test that free variables do not typecheck.
robrix Jan 12, 2016
912e8a7
Test the inference of bound variables.
robrix Jan 12, 2016
19b097a
Test that inferred types are checked.
robrix Jan 12, 2016
0d0358c
Test the inference of simple function types.
robrix Jan 12, 2016
57ad2a5
Simplify the test of simple function type inference.
robrix Jan 12, 2016
7c70635
Typecheck the bodies of lambdas.
robrix Jan 12, 2016
b3ed734
Add another test of simple function type inference.
robrix Jan 12, 2016
0e8a928
Test the inference of `identity`’s type.
robrix Jan 12, 2016
5ff72a4
Test the inference of `constant`’s type.
robrix Jan 12, 2016
4bb7cc4
Use the parameter type, and not its type, as the domain.
robrix Jan 12, 2016
318fea5
Shadow >> infix.
robrix Jan 12, 2016
90d1f24
Check lambdas against types.
robrix Jan 12, 2016
180c8fe
Make the >> definition available to all cases.
robrix Jan 12, 2016
c3bb9be
Strip some leading indentation.
robrix Jan 12, 2016
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Remove the Inferer/Checker synonyms.
  • Loading branch information
@robrix
robrix committed Jan 10, 2016
commit 2e7cd74e681958d0494bb94c3ab775feffb0f4fb
2 changes: 0 additions & 2 deletions src/Curve.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -116,8 +116,6 @@ maxBoundVariable = cata (\ expression -> case expression of
-- Typechecking

type Context = Map.Map Name Term'
type Inferer = Context -> Unification'
type Checker = Term' -> Inferer


-- Equality
Expand Down