[Haskell-cafe] Type-Level Programming

[Liam O'Connor]

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
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>