26 Jun
2010
26 Jun
'10
3:23 a.m.
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
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