4
$\begingroup$

In "Typing Haskell in Haskell", by Mark P. Jones, is provided a sort of haskell-like specification for typing Haskell. As stated in this paper, binding groups is a area "neglected in most theoretical treatments of type inference". Jones provided inference and checking algorithms for this syntactic construct, but it's typing rule is not referenced.

As far I know, binding groups is quite differente from usual let bindings. You can have mutual recursion, for example. Also, I don't know if is possible to simulate binding groups only using let expressions.

There is a typing rule for typing binding groups anywhere in the literature? If there is, then maybe the rest of this question is pointless.

This paper also doesn't give us a (in)formal grammar for the syntax, because it's goal is type inference/checking from the data stucture itself. I don't think this is strictly necessary, but a syntactic definition of binding groups may help defining a typing rule. So, I decided to give a sugestion of what this informal grammar may look like. Brackets means finite sequence and curly bracket means no-empty finite sequence.

Informa grammar

So, what I'm asking here is a rule for typing binding groups.

EDIT:

It seems that my question is not clear enough. I apologize for that. I'll try to make it more clear...

By typing rule (or type rule) I mean: en.wikipedia.org/wiki/Type_rule and by type checking algorithm I mean something easy to translate to code. I think the difference is more fundamental than just representation style. A rule is closer to a relation and an algorithm is closer to a function. What is missing is a rule, like in the wikipedia page, that could be used for certification of the algorithm.

Certification is the motivation behind my question. I want to certify the algorithms described in this paper.

|cite|improve this question
$\endgroup$
  • $\begingroup$ Don't post formulas as pictures, please. $\endgroup$ – Andrej Bauer Jan 11 at 16:17
3
+150
$\begingroup$

I don't know what rule Jones intended to use, but I'd guess it's something like

$$ \dfrac{ \Gamma' = \Gamma,x_1:\tau_1,\ldots,x_n:\tau_n \\ \Gamma' \vdash e_1 : \tau_1 \\ \cdots \\ \Gamma' \vdash e_n : \tau_n \\ \Gamma' \vdash e : \tau }{ \Gamma \vdash {\sf let}\ x_1=e_1;\cdots;x_n=e_n\ {\sf in}\ e : \tau } $$

which handles mutual recursion in groups. The rule above does not consider patterns as in x [p] = e, but it could be amended to support those as well.

I think binding groups are usually neglected since mutual recursion can be translated into non-mutual one (e.g. exploiting Bekić's theorem). However, in a real-world language it's convenient to have mutual recursion, even if from a purely theoretical point it's redundant. Hence, having a typing rule for it and an inference algorithm is still quite useful.

|cite|improve this answer
$\endgroup$
  • $\begingroup$ Does your rule also type alternatives? In Haskell you could write let len [] = 0; len (x:xs) = 1 + len xs. Note this is just one bind because is the same identifier and it has two alternatives. Your rule implicitly say that identifiers are different, because of the consistency of $\Gamma'$. So, in case of let x1 = e1; x1 = e2 in e, then what would happen with your rule? Does your rule guarantee that e1 and e2 have the same type? $\endgroup$ – Rafael Castro Jan 11 at 15:59
  • 2
    $\begingroup$ @RafaelCastro: The provided answer gets at the heart of the matter, the rest is mostly variation and techinique. The alternatives can be, for example, gathered together and treated as a siingle definition: let f p1 = e1; let f p2 = e2 becomes let f = \x -> case x of { p1 -> e1 ; p2 -> e2 }. There are probably further difficulties, but in a language with non-dependent types such as Haskell they can't be too big. $\endgroup$ – Andrej Bauer Jan 11 at 16:27
  • 1
    $\begingroup$ @RafaelCastro Ah, right. Likely, you want generalization (adding foralls) to be done after the whole group is checked, as it happens for single-definition lets. In real Haskell, the actual mechanism is a bit more complex since in a binding group some definitions might have explicit annotations while others have not. IIRC, Haskell puts the provided (polymorphic!) types in $\Gamma'$, and infers (monomorphic!) types for the rest, and then generalizes them at the very end. In the algorithm, there is even a loop-detecting pass to handle mutual recursion more carefully. $\endgroup$ – chi Jan 11 at 19:06
  • 1
    $\begingroup$ @RafaelCastro More Haskell details are here, but note that Haskell-specific subtleties should be discussed on StackOverflow. Here on CS.SE they are off-topic, as the details of any other programming language. General programming language theory is instead on-topic here. $\endgroup$ – chi Jan 11 at 19:10
  • 1
    $\begingroup$ @RafaelCastro Note that Haskell types both as Char->Char. I don't have any specific reference in mind. Perhaps Peyton-Jones papers/books can provide you more info about how it's done in Haskell. You could also check more general references (Hindley-Milner type system, algorithm W), even if I'm unsure about where one can find material on multiple bindings. BTW, I'd expect Bekić's theorem not to be used in a real compiler or any type inference algorithm. In practice, I think it's easier (and more efficient) to handle binding groups explicitly than resorting to Bekić's transformation. $\endgroup$ – chi Jan 16 at 18:52

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

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