Difference between revisions of "Simonpj/Talk:OutsideIn"
| Line 7: | Line 7: | ||
<blockquote> |
<blockquote> |
||
| − | '''Abstract'''. Advanced type system features, such as GADTs, type classes, and type families have have proven to be invaluable language extensions for ensuring data invariants and program correctness among others. Unfortunately, they pose a tough problem for type inference, becuase they introduce \emph{local} type assumptions. |
+ | <p>'''Abstract'''. Advanced type system features, such as GADTs, type classes, and type families have have proven to be invaluable language extensions for ensuring data invariants and program correctness among others. Unfortunately, they pose a tough problem for type inference, becuase they introduce \emph{local} type assumptions. |
| − | <p> |
+ | </p><p> |
In this article we present a novel constraint-based type inference approach for local type assumptions. Our system, called \OutsideIn{X}, is parameterised over the particular underlying constraint domain X, in the same way as HM(X). This stratification allows us to use a common metatheory and inference algorithm. |
In this article we present a novel constraint-based type inference approach for local type assumptions. Our system, called \OutsideIn{X}, is parameterised over the particular underlying constraint domain X, in the same way as HM(X). This stratification allows us to use a common metatheory and inference algorithm. |
||
| − | <p> |
+ | </p><p> |
Going beyond the general framework, we also give a particular constraint solver for X = type classes + GADTs + type families, a non-trivial challenge in its own right. |
Going beyond the general framework, we also give a particular constraint solver for X = type classes + GADTs + type families, a non-trivial challenge in its own right. |
||
| − | </blockquote> |
+ | </p></blockquote> |
This Wiki page is a discussion page for the paper. If you are kind enough to read this paper, please help us by jotting down any thoughts it triggers off. Things to think about: |
This Wiki page is a discussion page for the paper. If you are kind enough to read this paper, please help us by jotting down any thoughts it triggers off. Things to think about: |
||
Revision as of 14:53, 6 May 2010
Modular type inference with local assumptions: OutsideIn(X)
This epic 73-page paper (JFP style) brings together our work on type inference for type functions, GADTS, and the like, in a single uniform framework.
- Modular type inference with local assumptions: OutsideIn(X): PDF
- Related papers
Abstract. Advanced type system features, such as GADTs, type classes, and type families have have proven to be invaluable language extensions for ensuring data invariants and program correctness among others. Unfortunately, they pose a tough problem for type inference, becuase they introduce \emph{local} type assumptions.
In this article we present a novel constraint-based type inference approach for local type assumptions. Our system, called \OutsideIn{X}, is parameterised over the particular underlying constraint domain X, in the same way as HM(X). This stratification allows us to use a common metatheory and inference algorithm.
Going beyond the general framework, we also give a particular constraint solver for X = type classes + GADTs + type families, a non-trivial challenge in its own right.
This Wiki page is a discussion page for the paper. If you are kind enough to read this paper, please help us by jotting down any thoughts it triggers off. Things to think about:
- It is a long paper; where did you get lost?
- What is unclear?
- What is omitted that you'd like to see?
- Is there anything we could leave out?
You can identify your entries by preceding them with four tildes. Doing so adds your name, and the date. Thus:
- Simonpj 08:42, 19 April 2007 (UTC) Note from Simon
If you say who you are in this way, we'll be able to acknowledge your help in a revised version of the paper.