lost polymorphism in Typed Tagless Final Interpreters

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)

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