Programmers Stack Exchange is a question and answer site for professional programmers interested in conceptual questions about software development. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

Are there some theoretical reasons for that (like that the type checking or type inference would become undecidable), or practical reasons (too difficult to implement properly)?

Currently, we can wrap things into newtype like

newtype Pair a = Pair (a, a)

and then have Pair :: * -> *

but we cannot do something like λ(a:*). (a,a).

(There are some languages that have them, for example, Scala does.)

share|improve this question
Choosing one kind of type system into use excludes the other kind of type systems since the whole thing needs to be consistent. Type level lambda would be very strange in category theory... – tp1 Dec 1 '12 at 9:29
up vote 10 down vote accepted

Type inference with type level lambdas would require higher order unification which is undecidable. This is the motivation for disallowing them. But as has happened with other undecidable features (like type inference for GADTs), it might be possible to require type signatures and allow it. I'm not sure if that's been investigated by anyone.

share|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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