
26 Jun
2010
26 Jun
'10
7:27 a.m.
Stephen Tetley wrote:
On 26 June 2010 08:07, Andrew Coppin
wrote: Out of curiosity, what the hell does "dependently typed" mean anyway?
How about:
"The result type of a function may depend on the argument value" (rather than just the argument type)
Hmm. This sounds like one of those things where the idea is simple, but the consequences are profound... (I have once or twice wanted to do this in fact, but I don't recall why now.)