[Haskell-cafe] Type-Level Programming
liamoc at cse.unsw.edu.au
Sat Jun 26 03:23:44 EDT 2010
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 <andrewcoppin at 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 at haskell.org
More information about the Haskell-Cafe