[Haskell-cafe] Type-Level Programming

[Tony Morris]

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


-- 
Tony Morris
http://tmorris.net/