Take the 2-minute tour ×
Programmers Stack Exchange is a question and answer site for professional programmers interested in conceptual questions about software development. It's 100% free, no registration required.

The questions all the title. Just to clarify, Haskell already has the ability to parametise a type over another type (this is just like template programming in c++), but can it parametise a type over values - this is a dependent type. So for example you can have a type thats parametised over the integers, for example vectors of size n, matrices of size n x m, etc.

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

share|improve this question
add comment

2 Answers

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
add comment

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
add comment

Your Answer

 
discard

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.