5
$\begingroup$

I have seen stated in various places that in order to allow an "increase in polymorphism," functional dependency analysis should be performed, and type inference should be used for every declaration group in topological order. It seems like a well-known fact... except that nobody provides any reference or example.

In fact I don't understand what is really meant by this statement. Does it mean that without doing dependency analysis I wouldn't be able to type some programs (i.e. some valid programs would fail type-checking) or only that I would type them with a type that is more specific than what really is?

I'm particularly interested in consequences in a Haskell-like language/type system. In particular during kind inference, is dependency analysis actually necessary to avoid rejecting valid programs? Can you provide an example that wouldn't be well-kinded if typed without performing dependency analysis?

Since kinds are monomorphic I struggle to understand why dependency analysis should matter in this particular case.

$\endgroup$
2
$\begingroup$

Any use of a type anywhere may place constraints on that type. So, in the absence of explicit type signatures (i.e. when doing type inference) it is necessary to perform inference in a way that doesn't allow specific usages of a type in a particular form to "infect" the most general type it may have. This involves a dependency analysis. Consider

id = \x -> x
foo = id 1

Now if we type foo first, we would unify the first argument of id with Int and thus conclude id had type Int -> Int. So therefore we must first type id and then generalize its signature to the polymorphic type forall a. a -> a, and then instantiate that at type Int when we apply it and attempt to unify the argument type with Int.

Hence, dependencies and topological sort!

$\endgroup$
  • $\begingroup$ Yes, but this doesn't answer the second part of my question. What if the language is not polymorphic (e.g. the kinds in Haskell 98). Does not using dependency analysis "kind" incorrectly some programs or not "kind" at all some well-kinded programs? $\endgroup$ – Bakuriu Oct 9 '14 at 4:57
  • $\begingroup$ @Bakuriu The Haskell report gives an example where the choice of what dependencies to include in kind analysis makes a difference haskell.org/onlinereport/decls.html#kindinference $\endgroup$ – Sterling Clover Oct 13 '14 at 1:46

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.