漂亮的印刷与免费monad和GADT

Question

考虑由以下GADT定义的表达式函子：

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
import Control.Monad.Free
data ExprF :: * -> * where
  Term :: Foo a -> (a -> r) -> ExprF r
instance Functor ExprF where
  fmap f (Term d k) = Term d (f . k)
type Expr = Free ExprF

其中Foo被定义为

data Foo :: * -> * where
  Bar :: Int    -> Foo Int
  Baz :: Double -> Foo Double
instance Show a => Show (Foo a) where
  show (Bar j) = show j
  show (Baz j) = show j

ExprF中的(a -> r)字段和限制性GADT构造函数的组合似乎使编写一个漂亮的打印解释器变得不可能：

pretty (Pure r)          = show r
pretty (Free (Term f k)) = "Term " ++ show f ++ pretty (k _)

类型孔是人们所期望的：

Found hole ‘_’ with type: a1
Where: ‘a1’ is a rigid type variable bound by
            a pattern with constructor
              Term :: forall r a. Foo a -> (a -> r) -> ExprF r,
            in an equation for ‘pretty’
            at Test.hs:23:15
Relevant bindings include
  k :: a1 -> Free ExprF a (bound at Test.hs:23:22)
  f :: Foo a1 (bound at Test.hs:23:20)
  pretty :: Free ExprF a -> String (bound at Test.hs:22:1)
In the first argument of ‘k’, namely ‘_’
In the first argument of ‘pretty’, namely ‘(k _)’
In the second argument of ‘(++)’, namely ‘pretty (k _)’

似乎没有办法为continuation提供所需类型的值。该类型在f中编码，我正在使用的其他解释器以某种方式处理f，以提取适当类型的值。但通往String表示的道路似乎被阻断了。

这里有我遗漏的一些常用成语吗？如果真的有可能的话，如何漂亮地打印Expr的值呢？如果不可能，ExprF的哪种替代结构可能会捕获相同的结构，但也支持漂亮的打印机？

Answer 1

只有f上的模式匹配。如果这样做，k的类型将被细化，以匹配Foo:中包含的类型

pretty (Pure r)          = show r
pretty (Free (Term f k)) = "Term " ++ show f ++ pretty r where
  r = case f of
    Bar a -> k a
    Baz a -> k a

你可能想排除这种模式：

applyToFoo :: (a -> r) -> Foo a -> r
applyToFoo f (Bar a) = f a
applyToFoo f (Baz a) = f a
pretty (Pure r)          = show r
pretty (Free (Term f k)) = "Term " ++ show f ++ pretty (applyToFoo k f)

Answer 2

这并非不可能。至少你可以在f:上进行模式匹配

pretty :: (Show a) => Expr a -> String
pretty (Pure r) = show r
pretty (Free (Term f@(Bar x) k)) = "Term " ++ show f ++ pretty (k x)
pretty (Free (Term f@(Baz x) k)) = "Term " ++ show f ++ pretty (k x)

但这并不是很令人满意，因为您已经在Foo的show实例中这样做了。

因此，挑战在于适当地抽象。