Lennart Augustsson writes:
> Wolfram Kahl wrote:
>
> > In the end, my dreams even include a proof format
> > that can be checked by the compiler :-)
>
> Dependent types! That's all you need.
Absolutely!
I have read your Cayenne paper
( http://www.cs.chalmers.se/%7Eaugustss/cayenne/paper.ps )
and in that light the proposals made in this thread seem clunky and lame.
Why kludge around with things like this if we can have dependent types ?
I ask the above question seriously, since I haven't seen Simon's original
post. Would it be hard to implement dependent types for ghc (keeping in mind
that the high payoff would justify some effort) ?
Tim
