CODEWITHSUNDEEP
haskelltype-inferencetype-systemsgadt
Jason Dagit
Jason Dagit

Reputation: 13844

Fundeps and GADTs: When is type checking decidable?

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!

Upvotes: 16

Views: 1269

Answers (2)

Jude Allred
Jude Allred

Reputation: 11057

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 :-)

Upvotes: 9

Nick Fortescue
Nick Fortescue

Reputation: 44153

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.

Upvotes: 1

Related Questions