Simonpj/Talk:OutsideIn

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. Version 3 (camera ready copy for JFP) is very substantially revised compared to the May 2010 version.

• OutsideIn(X) - Modular type inference with local assumptions: PDF
• Related papers (constraints)
• Related papers (GADTs)
• Related papers (type families)

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, because they introduce 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.

Please help us!. 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.

Heisenbug 17:42, 8 February 2011 (UTC) Note from Gabor Greif

Just found this paper and had a quick look. You should probably compare your algorithm with Algorithm-P described in Chuan-kai Lin's PhD thesis where he claims to have developed a practical algorithm for GADT type inference. The work presumably obsoletes both references mentioned here to Lin's and Sheard's papers.

---

---

Version 1 comments, now dealt with; thank you!

Simon Meier 15 May 2010:

• Typo on Page 7: "having type Bool" should probably be "having type Int".
• Typo on Page 18: "constraint siplifier"
• Typo on Page 28: "topl-level"
• Typo on Page 31: "But hang on! NoGen means ... in the beginning of Section 4.2 <text-missing-here>"
• Typo on Page 53: Formula below "Simplification rules" is missing a space.
• Typo on Page 59: "makes sens"

Batterseapower 14:24, 14 May 2010 (UTC) You say that local definitions such as "combine" and "swap" could harmlessly be defined at top level. However, there is a cost to doing so in that it pollutes the top-level namespace. Adding a facility for making definitions that are at the top level for the purposes of type checking but not for name resolution would fix this, at the cost of some ugliness.

Rgreayer 16:04, 14 May 2010 (UTC)

• Revisiting Typo on Page 7: "This means that any expression of type F [Bool] can be considered an expression of type F Bool". But would that not mean the axiom is: F [a] ~ F a, rather than: F [a] ~ a?
• Typo, Page 8 (middle): "An similar issue..."

Saizan 14:23, 16 May 2010 (UTC)

• Figure 2: VarCon uses \nu in the conclusion and x in the premises, it seems they should both be \nu considering the textual description below, but then the definition of "Type environments" in Figure 1 also needs to have \nu rather than x.
• typos in Section 9.1:
  • "f = case (Ex 3) of Ex -> False" should be "f = case (Ex 3) of Ex _ -> False".
  • "f :: Bool -> Bool" should be "f :: Bool".
• Have you considered adding support for partial type signatures?

niall 15:07, 17 May 2010 (UTC)

• Footnote on page 65 refers to an incorrect link (should perhaps be http://research.microsoft.com/en-us/um/people/simonpj/papers/gadt/ ) although the journal paper does not seem linked from there. The Appendix with the algorithm is perhaps meant to refer to the appendix of "Simple unification-based type inference for GADTs"?

Byorgey 09:10, 21 June 2010 (UTC)

• p.8: should be a colon after "Here is an example"
• p.10: end of section 2.2: "definition of g" should be "definition of test"
• p.15: Indentation of "The judgement Q ; Gamma |- prog..." is too small
• p.16: Grammar of Definition 3.1 needs fixing, for example, "An axiom scheme Q is consistent iff whenever ... *we have* (or, *it is also the case that*, etc.)
• p.17: add comma after however in "For now, however algorithmic constraints..."
• p.19: in Fig 7, should the Empty rule have a premise ftv(Q,Gamma) = empty?
• p.21: I find it very confusing to use the notation t1 <= t2 for "t1 is more general than t2"; we are using a "less than" symbol for a concept involving the word "more"... Also, it took me a long time to grok details of the definition of "more general than", since it's contravariant in the constraints etc... it might be nice to add a paragraph giving a bit more explanation/intuition for this definition.
• p.23, section 3.7: "Haskell type checker usually transform the program"
• p.25: "...explain those modifications in Section 4 and Section 4.2" -- is the "Section 4" correct?
• p.28: "...we abstract over the (Show a) constraint even though g is not polymorphic..." should be h instead of g?
• p.29: "will hardly be delirious": delirious is a strange word choice, not sure what you are trying to convey.
• p.31: "It is not enough to pick out equality constraints..." I find this section unclear. Perhaps a bit more detail would be helpful?
• p.31: "But hang on! NoGen ..." incomplete sentence, and I do not know which f function you are referring to.
• p.36: Period missing at the end of item 2.
• p.37: In the first bullet point, missing comma after tau.
• p.37: "This is obviously..." please drop "obviously", it is not obvious to me!
• p.38: Fig. 13: There are two places where .tau_1 appear in LetA; what does this notation mean?
• p.39: "Subsequently we may recursively solves"
• p.40: last sentence of section 5.5, "being in domain of theta", add "the"
• p.40, Lemma 5.1: "for all" instead of "forall"
• p.45: Sentence "What this means is that ... typing rules" does not make sense. Also, foo is not a good example because in this *particular* case, the algorithm COULD detect the inconsistency.
• p.46: first sentence, "The return type of foo..." is rather confusingly worded.
• p.46: "between the programs typed the algorithm" add "by"
• p.49, section 7.1: You should be more cafeul with the terms "type family", "type function", "function", "function-free"; I was initially confused and thought "function" and "function-free" was referring to function types like a -> b. For example at the top of page 49, "GHC enforces that type family instance declarations involve only functions applied to function-free types"... this confused me a lot at first, I was unsure why GHC would not allow arrow types in type family instance declarations!
• p.49: "Given this syntax of constraints, Figure 17 gives..." should be Figure 18?
• p.50: "for ever" should be "forever"
• p.53, Fig. 20: In the definition of <_alpha, in the first case, what if tau = G vs? And how does a var compare to a non-var, and so on?
• p.55, Fig. 21: Suppose we had an equality F x y z ~ G a b c, how would it be flattened? It seems we need to flatten away the application of G from the RHS but I do not see how the given rules accomplish, since they seem to only flatten things which are *arguments* to type functions on both sides.
• p.56: "would get two new constraints: F beta ~ Int `union` G Int beta", missing a twiddle, should be G Int ~ beta
• p.57, Fig 22: Why do we have both DDICTG and DDICTW? They seem identical.
• p.57, Fig 22 (and Fig 23): given constraints F Int ~ a and a ~ Bool, should this be rewritten to F Int ~ Bool and a ~ Bool? Or does this not matter? There don't seem to be rules to accomplish this.
• p.58: "...and a wanted constraint F Int a", missing a twiddle
• p.59: the typesetting of |->s is strange, there needs to be more space after |->s since it currently overlaps with whatever comes after it
• p.67: "NoQual is a no-option" -- probably better to say "is not an option"

Longlivedeath 03:11, 15 July 2010 (UTC)

• In the References section: replace "Fun with type fnnctions" to "Fun with type functions"

Jobo 12:07, 20 July 2010 (UTC) I just took a quick look at the references section:

• There are some referenses to a Mr Jones, Simon Peyton.
• References in the paper read etal. or et al, shold be et al. (two words, ending in a dot).
• Some references have the form "Sulzman et al. (Sulzmann et al. 2006); consider using \citet.