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?
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.
2
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)”
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:
- https://www.youtube.com/watch?v=O805YjOsQjI
- https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell
- https://github.com/goldfirere/ghc/