On Fri, Dec 23, 2005 at 03:34:40AM -0000, [EMAIL PROTECTED] 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 _______________________________________________ Haskell mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell
