16

I was reading a research paper about Haskell and how HList is implemented and wondering when the techniques described are and are not decidable for the type checker. Also, because you can do similar things with GADTs, I was wondering if GADT type checking is always decidable.

I would prefer citations if you have them so I can read/understand the explanations.

Thanks!

Don Stewart
  • 137,316
  • 36
  • 365
  • 468
Jason Dagit
  • 13,684
  • 8
  • 33
  • 56
  • 1
    This question might be better directed to the authors of the research paper. It's a bit esoteric for Stack Overflow. (I've always had great success contacting researchers for comment. They're usually ecstatic *anybody* is reading their work.) – Chris Conway Sep 07 '08 at 23:58
  • 7
    I think this attitude (that theoretical questions have no bearing on a pragmatic forum) is harmful and obsolete. Pragmatic approaches should be open to new technologies, because those technologies can likely improve daily activities in the near future. eg: functional features in c#/python. – rcreswick Sep 08 '08 at 01:30
  • That said, Chirs's comment is probably right-on, practically speaking. I wish it weren't though. – rcreswick Sep 08 '08 at 01:32
  • rcreswick: I don't think the question has no bearing. I just don't think the Stack Overflow community is likely to produce a satisfactory answer. – Chris Conway Sep 08 '08 at 03:55

2 Answers2

9

I believe GADT type checking is always decidable; it's inference which is undecidable, as it requires higher order unification. But a GADT type checker is a restricted form of the proof checkers you see in eg. Coq, where the constructors build up the proof term. For example, the classic example of embedding lambda calculus into GADTs has a constructor for each reduction rule, so if you want to find the normal form of a term, you have to tell it which constructors will get you to it. The halting problem has been moved into the user's hands :-)

Jude Allred
  • 10,977
  • 7
  • 28
  • 27
1

You've probably already seen this but there are a collection of papers on this issue at Microsoft research: Type Checking papers. The first one describes the decidable algorithm actually used in the Glasgow Haskell compiler.

Nick Fortescue
  • 43,045
  • 26
  • 106
  • 134