[Haskell] Re: A question about fundeps <-> GADT interaction

[Tomasz Zielonka]

On Fri, Dec 23, 2005 at 03:34:40AM -0000, oleg at pobox.com wrote:
> 
> [Sorry for possible duplication, our DNS server seems to be broken,
>  and the sysadm is on vacation]
> 
> I don't think that is the problem with GADTs. The following works
> 
> > untype :: Term f a -> Term Untyped ()
> > untype (Lit x)      = Lit x
> > untype (Succ t)     = Succ (untype t)
> > untype (IsZero t)   = IsZero ((untype t)::Term Untyped ())
> > untype (If c t e)   = If ((untype c)::Term Untyped ()) 
> >		           ((untype t)::Term Untyped ())
> >		           ((untype e)::Term Untyped ())
> 
> Here's a more extensive example:
> 
> > tlit :: Int->Term Typed Int
> > tlit = Lit
> >
> > [l0,l1,l2] = map tlit [0..]
> >
> > --ex2 :: Term Untyped ()
> > ex2' =
> >     If  (IsZero (Succ (Lit 0)))
> >         (untype l1)
> >         (IsZero (untype l2))
> 
> ex2' of course won't typecheck if `untype' are removed.

Great! Thanks! :-)

Could you explain why additional type annotations are required?

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