It means that not only can values have types, types can have values. An example of the uses of a dependent type would be to encode the length of a list in it's type.
Due to the curry-howard isomorphism, dependent types open the gateway for lots of type-level theorem proving. On 26 June 2010 17:07, Andrew Coppin <andrewcop...@btinternet.com> wrote: > wren ng thornton wrote: >> >> And, as Jason said, if you're just interested in having the same >> programming style at both term and type levels, then you should look into >> dependently typed languages. > > Out of curiosity, what the hell does "dependently typed" mean anyway? > > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
