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

I know Haskell already has the ability to parametrise a type over another type (similar to template programming in C++), but I'm wondering whether Haskell can also parametrise a type over values – whether it supports dependent types. With dependent types, you can have a type that's parametrised over integers, for example vectors of size n, matrices of size n×m, etc.

If not, why not? And is there any possibility that it will be supported in the future?

share|improve this question

Haskell doesn't quite have full dependent types, although it can get very close with extensions like DataKinds and TypeFamilies. The issue at the moment, as far as I know, is that value-level Haskell has explicit bottoms but type-level Haskell does not.

This doesn't stop you from parametrizing types over other types, including the DataKind-lifting of values. As of GHC 7.6, and with DataKinds enabled, you can use type-level naturals and strings, as well as type-level tuples, type-level lists, and the type-level liftings of any (non-higher-kinded, non-generalized, non-constrained) algebraic data types, which is similar to (but much more general than) C++'s ability to use integers in templates.

share|improve this answer
Do the upcoming changes in GHC 8 add full dependent types? – Janus Troelsen Feb 15 at 0:02
@JanusTroelsen Not quite; they enable dependent kinds. – Ptharien's Flame Feb 15 at 1:01

To expand a bit on what Ptharien's Flame explained nicely about the current status - and GHC Haskell seems to be moving further in the direction of dependent types (while preserving phase separation) with each version.

So for eg at ICFP 2013 this September, a paper on the next phase of this process should be presented, "Towards dependently typed Haskell: System FC with kind equality", about collapsing the kind and type levels. As was announced to be the plan some 3 years ago.

And it even mentions the next step: "We are also aware that Adam Gundry’s forthcoming dissertation will include Π-types in a version of System FC and we will want to make this feature available in the source language as well. (Personal communication)"

share|improve this answer

Haskell has traditionally tried to fake it, but the end result is a much larger and seemingly repetitive type system. But this might soon change! See:

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.