[Haskell] Re: Conditional typechecking with GADTs

[Tomasz Zielonka]

On Tue, Dec 27, 2005 at 08:07:39PM -0800, oleg at 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