
26 Jun
2010
26 Jun
'10
7:31 a.m.
http://www.cs.nott.ac.uk/~txa/publ/ydtm.pdf Andrew Coppin wrote:
Liam O'Connor wrote:
It means that not only can values have types, types can have values.
Uh, don't types have values *now*?
An example of the uses of a dependent type would be to encode the length of a list in it's type.
Oh, right. So you mean that as well as being able to say "Foo Bar", you can say "Foo 7", where 7 is (of course) a value rather than a type. (?)
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
-- Tony Morris http://tmorris.net/