22 Nov
2009
22 Nov
'09
1:08 p.m.
Brent Yorgey wrote:
"free theorem" will be of the form
"Any function f of type T, *no matter how f is implemented*, will always satisfy the following property:
blah blah f blah = blah f blah "
This has nothing to do with whether or not there is only one possible implementation of f that does not involve undefined, which is a different phenomenon.
If it hasn't been mentioned, djinn turns type signatures into code, as has been discussed, although if f has multiple implementations, it will simply produce one of them. http://hackage.haskell.org/package/djinn The discussion on ltu helps flesh out the concept: http://lambda-the-ultimate.org/node/1178 This is, of course, as Brent pointed out, very different from free theorems. --S