Re: lost polymorphism in Typed Tagless Final Interpreters

fromTree :: Tree -> Either ErrMsg (forall repr. ExpSYM repr => repr)
fromTree (Node "Lit" [Leaf n]) = (\x -> lit x) <$> (safeRead n)
fromTree (Node "Neg" [e]) = (\x -> neg x) <$> (fromTree e)
fromTree (Node "Add" [e0, e1]) =  (\x y -> add x y) <$> (fromTree e0) <*> (fromTree e1)
fromTree e = Left ("Invalid tree: " ++ show e)

tf1' :: Either ErrMsg (forall repr . ExpSYM repr => repr)
tf1' = fromTree tf1_tree

Explanation:

Either ErrMsg Wrapped becomes Either ErrMsg (forall r. ExpSYM r => r)

GHC's impredicativity doesn't understand some partial applications and 
pointfree code (it's too hard). So change lit <$> safeRead n to (\x -> 
lit x) <$> safeRead n, for example.

On 2025-11-11 18:19, Anthony Carrico via Haskell-Cafe wrote:
> In his tutorial lecture "Typed Tagless Final Interpreters"
>
> https://www.okmij.org/ftp/tagless-final/course/lecture.pdf
>
> Oleg Kiselyov deals with the issue of losing polymorphism,
>
> tf1'_both :: IO()
> tf1'_both =
>   case tf1' of
>     Left e -> putStrLn ("Error: " ++ e)
>     Right (x) -> do
>       print (eval x)
>       print (view x)
>
> "We have lost polymorphism. The problem is subtle: the function 
> fromTree is indeed polymorphic over repr, as its inferred type shows. 
> However, to extract the de-serialized term, we have to do 
> pattern-matching; the variable x is bound in the case pattern and 
> hence, like a lambda-pattern–bound variable, gets a monomorphic, 
> non-generalizable type. Therefore, we cannot interpret x with several 
> arbitrary interpreters; the extensibility is lost."
>
> He shows how to use a newtype wrapper to work around the issue, but 
> also says in a foot note:
>
> "With the impredicative polymorphism GHC extension, we do not have to 
> fake first-class polymorphism and do not need Wrapped."
>
> Two questions:
>
> 1. Is this true? I still get the error.
>
> 2. Can anyone summarize the current state of this issue today?
>
> It can be hard follow the issue through the history of Haskell/GHC.
>
> Thanks to Oleg for publishing this lecture, it is possible to learn 
> quite a bit from it, and thanks to whoever would like to give an update!
>
> I've smashed together my source code from the F module and the 
> Serialization module together below. You can see the "defered type 
> error" at the very bottom.
>
> $ ghc --version
> The Glorious Glasgow Haskell Compilation System, version 9.8.4
>
> {-# LANGUAGE NoMonomorphismRestriction #-}
> {-# LANGUAGE FlexibleInstances #-}
> {-# LANGUAGE ImpredicativeTypes #-}
>
> module F where
>
> class ExpSYM repr where
>   lit :: Int -> repr
>   neg :: repr -> repr
>   add :: repr -> repr -> repr
>
> instance ExpSYM Int where
>   lit n = n
>   neg e = -e
>   add e0 e1 = e0 + e1
>
> eval :: Int -> Int
> eval = id
>
> instance ExpSYM String where
>   lit n = show n
>   neg e = "(-" ++ e ++ ")"
>   add e0 e1 = "(" ++ e0 ++ " + " ++ e1 ++ ")"
>
> view :: String -> String
> view = id
>
> data Tree = Leaf String
>             | Node String [Tree]
>             deriving (Eq, Read, Show)
>
> instance ExpSYM Tree where
>   lit n = Node "Lit" [Leaf (show n)]
>   neg e = Node "Neg" [e]
>   add e0 e1 = Node "Add" [e0, e1]
>
> toTree :: Tree -> Tree
> toTree = id
>
> type ErrMsg = String
>
> safeRead :: Read a => String -> Either ErrMsg a
> safeRead s = case reads s of
>                [(x, "")] -> Right x
>                _ -> Left $ "Read error: " ++ s
>
> fromTree :: (ExpSYM repr) => Tree -> Either ErrMsg repr
> fromTree (Node "Lit" [Leaf n]) = lit <$> (safeRead n)
> fromTree (Node "Neg" [e]) = neg <$> (fromTree e)
> fromTree (Node "Add" [e0, e1]) =  add <$> (fromTree e0) <*> (fromTree e1)
> fromTree e = Left ("Invalid tree: " ++ show e)
>
> tf1 :: ExpSYM repr => repr
> tf1 = add (lit 8) (neg (add (lit 1) (lit 2)))
>
> tf1_tree :: Tree
> tf1_tree = toTree F.tf1
>
> tf1' :: ExpSYM repr => Either ErrMsg repr
> tf1' = fromTree tf1_tree
>
> tf1'_eval :: IO()
> tf1'_eval =
>   case tf1' of
>     Left e -> putStrLn ("Error: " ++ e)
>     Right x -> print (eval x)
>
> -- >>> tf1'_eval
> -- 5
>
> tf1'_view :: IO()
> tf1'_view =
>   case tf1' of
>     Left e -> putStrLn ("Error: " ++ e)
>     Right x -> print (view x)
>
> -- >>> tf1'_view
> -- "(8 + (-(1 + 2)))"
>
> tf1'_both :: IO()
> tf1'_both =
>   case tf1' of
>     Left e -> putStrLn ("Error: " ++ e)
>     Right (x) -> do
>       print (eval x)
>       print (view x)
>
> -- >>> tf1'_both
> -- *** Exception: /tmp/danteIpH3fg.hs:90:19: error: [GHC-83865]
> --     • Couldn't match type ‘Int’ with ‘[Char]’
> --       Expected: String
> --         Actual: Int
> --     • In the first argument of ‘view’, namely ‘x’
> --       In the first argument of ‘print’, namely ‘(view x)’
> --       In a stmt of a 'do' block: print (view x)
> -- (deferred type error)
>

_______________________________________________
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.