There has been extensive discussion of whether Haskell has dependent types, made larger by the fact that the definition of dependently-typed languages is a bit fuzzy. On some accounts, type functions or GADTs are sufficient for calling a language dependently-typed, and Haskell got both features. The situation is clearer with linear types. First of all, Haskell has all facilities for statically ensuring the proper use of resources. The simplest example is enforcing the locking protocol: a lock can be acquired no more than once; only acquired locks may be released, all acquired locks must be released at the end. This simple example is described in Sec 5.2 of http://research.microsoft.com/en-us/um/people/simonpj/papers/assoc-types/fun... That example can be made more complex: a program with two locks choosing the lock to acquire based on the data it reads from a file. We can still statically guarantee that all acquired locks are released and no lock is acquired or released twice -- even if we cannot statically tell which particular lock will be acquired during a program run. Other examples of resource control include session types and regions. There are several Hackage packages with these keywords. Generally, Haskell can easily embed languages with dependent or linear types -- just as easily as Haskell embeds languages with IO, global mutable state, non-determinism. The latter languages go by the name of monads. One can easily embed typed linear lambda-calculus, with Haskell type-checker ensuring that each bound variable is referenced exactly once. http://okmij.org/ftp/tagless-final/course/index.html#linear The linear lambda-calculus turns out not very useful; no wonder Girard had to add exponentials.