[Haskell-cafe] linear and dependent types

oleg at okmij.org oleg at okmij.org
Sat Feb 19 08:31:08 CET 2011


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-with-type-funs/typefun.pdf

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.




More information about the Haskell-Cafe mailing list