Changes between Version 1 and Version 2 of Typechecking


Ignore:
Timestamp:
Feb 12, 2016 2:00:10 PM (4 years ago)
Author:
goldfire
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Typechecking

    v1 v2  
    11This page is to track thoughts about the core type-checking (constraint-generation) algorithm.
    22
    3 = Current state (Oct 2015) =
     3= Current state (Feb 2016) =
     4
     5Much of this proposal (without `ExpFun`) is now in HEAD and 8.0.
     6
     7= Previous state (Oct 2015) =
    48
    59GHC claims to do bidirectional type-checking, but it doesn't quite do this. In a proper bidirectional type-checking algorithm (as in [http://repository.upenn.edu/cis_papers/315/ the "Practical Type Inference" paper]), the algorithm is either in "infer" mode or "checking" mode, never both. But GHC uses more of a mixed economy.
     
    5155The other place where it comes up is in dealing with rebindable syntax. For example, we want to type-check `negate` against `hole1 -> hole2`. Perhaps by having the arrow in the structure, type inference could make more progress than it could otherwise.
    5256
    53 '''Current status''': Richard has started this, but got stuck on the rebindable syntax bit because he was missing `ExpFun`. The work-in-progress is at `github.com/goldfirere/ghc` on the `bidir-refactor` branch. Simon and Richard both seem to think this would be a good idea. Richard may do this in due course.
    54 
    5557== A specification ==
    5658