29 May
2008
29 May
'08
9:21 a.m.
Kim-Ee Yeoh
Luke Palmer-2 wrote:
You have now introduced a first-class type function a la dependent types, which I believe makes the type system turing complete. This does not help the decidability of inference :-)
God does not care about our computational difficulties. He infers types emp^H^H^H ... uh, as He pleases.
This begs the question: Can God come up with a type He doesn't understand? The answer, it seems, is Mu. -- (c) this sig last receiving data processing entity. Inspect headers for past copyright information. All rights reserved. Unauthorised copying, hiring, renting, public performance and/or broadcasting of this signature prohibited.