On Tue, Dec 27, 2005 at 08:07:39PM -0800, oleg@pobox.com wrote:
Tomasz Zielonka wrote:
The papers on GADTs have an example showing how you can transform, traverse and evaluate ASTs (or terms) with more type safety. I've used such an approach in one of my applications and it works remarkably well.
However, I would like to be able to "turn off" that type-safety in some parts of code, for example to separate parsing from typing. I thought I found a way to do this, because I was able to create Typed (with all consistency checking) and Untyped (without consistency checking) terms. Unfortunately I seem to be unable to write any useful function on such terms - GHC complains that there are type errors.
The present message shows what seems to be a more fruitful approach to writing terms whose typechecking can be `postponed', perhaps indefinitely. The approach tries to play to the strengths of GADTs and avoid their weaknesses. [...]
Wow! This is cool! But I'm not sure how far I can go with this approach. I'll see if this can be used to separate parsing from type-checking. Best regards Tomasz -- I am searching for a programmer who is good at least in some of [Haskell, ML, C++, Linux, FreeBSD, math] for work in Warsaw, Poland