Re: lost polymorphism in Typed Tagless Final Interpreters

On 11/11/25 22:09, Albert Y. C. Lai wrote:
> fromTree :: Tree -> Either ErrMsg (forall repr. ExpSYM repr => repr)

Thank you, so move the constraint:
   fromTree :: (ExpSYM repr) => Tree -> Either ErrMsg repr

like this:
   fromTree :: Tree -> Either ErrMsg (forall repr . ExpSYM repr => repr)

which yields this:
-- >>> tf1'_eval
-- *** Exception: /tmp/danteIpH3fg.hs:63:34-36: error: [GHC-39999]
--     • No instance for ‘ExpSYM (forall repr. ExpSYM repr => repr)’
--         arising from a use of ‘lit’
--     • In the first argument of ‘(<$>)’, namely ‘lit’
--       In the expression: lit <$> (safeRead n)
--       In an equation for ‘fromTree’:
--           fromTree (Node "Lit" [Leaf n]) = lit <$> (safeRead n)
-- (deferred type error)

and then wrap the ExpSYM members:
   fromTree (Node "Lit" [Leaf n]) = lit <$> (safeRead n)

in lambdas like this:
   fromTree (Node "Lit" [Leaf n]) = (\x -> lit x) <$> (safeRead n)

and it works--Nice work Albert!

I haven't yet tried to see if this version of the solution survives 
Oleg's extensibility challenge:

"To wrap a term of an extended language with multiplication, we need the 
MulSYM repr constraint..."

Is there perhaps a way to solve these problems with type annotations or 
the GHC TypeApplications extension at the point where they crop up? For 
example here:

tf1'_both =
   case tf1' of
     Left e -> putStrLn ("Error: " ++ e)
     -- ISSUE: the bound variable x here in the pattern match gets a
     -- monomorphic type.
     Right (x) -> do
       print (eval x)
       print (view x)

A type application or annotation on x would be much better documentation 
about polymorphism issues in the code than wrapping the ExpSYM methods 
in lambdas which seems ingenious, but rather random.

Without being an export in type systems, it is hard to figure out just 
where these edges are, but if the problems are with type inference, 
rather that the type system itself, it seems like they could be resolved 
with hints to the type checker.

Maybe this type of programming is still too far out on a limb to really 
work well in Haskell, but I'd love to better understand Haskell's 
progress on the issues. I think that seeing return type polymorphism in 
this same lecture of Oleg's some years ago was the thing that first got 
me interested in Haskell, so even though it involves impredicative 
types, it is actually kind of a beginners question that I'm returning to 
now--the possibilities of using such polymorphism attracted me to the 
language.

Thanks again for helping me understand!

-- 
Anthony Carrico

_______________________________________________
Haskell-Cafe mailing list -- [email protected]
To (un)subscribe, modify options or view archives go to:
Only members subscribed via the mailman list are allowed to post.