如何“显示”不可显示的类型？

Question

我正在使用data-reify并将graphvizeDSL 转换为一个很好的图形表示，用于内省。

作为一个简单的、人为的例子，请考虑：

{-# LANGUAGE GADTs #-}

data Expr a where
  Constant :: a -> Expr a
  Map :: (other -> a) -> Expr a -> Expr a
  Apply :: Expr (other -> a) -> Expr a -> Expr a

instance Functor Expr where
  fmap fun val = Map fun val

instance Applicative Expr where
  fun_expr <*> data_expr = Apply fun_expr data_expr
  pure val = Constant val

-- And then some functions to optimize an Expr AST, evaluate Exprs, etc.

为了使内省更好，我想打印存储在 DSL 数据类型的某些 AST 节点内的值。但是，通常任何a可能存储在 中Constant，即使那些没有实现Show. 这不一定是一个问题，因为我们可以限制Expr像这样的实例：

instance Show a => Show (Expr a) where
  ...

然而，这不是我想要的：我仍然希望能够打印，Expr即使a不是Show-able，通过打印一些占位符值（例如只是它的类型和它不可打印的消息）。

因此，如果我们有一个aimplementation Show，我们想要做一件事，如果一个特定的a没有，则另一件事。

此外，DSL 也有构造函数Map，Apply这甚至更成问题。构造函数在 中是存在的other，因此我们不能对other,a或 做任何假设(other -> a)。添加约束类型other的MapRESP。Apply构造函数会破坏Functorresp的实现。Applicative转发给他们。

但在这里我也想打印这些功能：

• 一个独特的参考。这始终是可能的（即使它是不漂亮，因为它需要unsafePerformIO使用）System.Mem.StableName。
• 它的类型，如果可能的话（一个技术是使用show (typeOf fun)，但它要求fun是Typeable）。

我们再次遇到了一个问题，如果我们有一个f实施，我们想做一件事，如果没有Typeable，另一件事f。

这该怎么做？

---

额外免责声明：这里的目标不是为Show不支持它的类型创建“正确”的实例。没有愿望Read以后能够他们，或者print a != print b暗示a != b。

目标是以“适合人类内省”的方式打印任何数据结构。

我被困在的部分是，如果额外的约束对aresp持有，我想使用一种实现。(other -> a)，但如果这些不存在，则为“默认”。也许FlexibleInstances这里需要类型类，或者类型族？我一直无法弄清楚（也许我一起走错了轨道）。

Answer 1

事实证明，这是一个过去已经被很多人认识到的问题，被称为“约束单子问题”。有一个优雅的解决方案，在Neil Sculthorpe、Jan Bracker、George Giorgidze 和 Andy Gill 的论文The Constrained-Monad Problem中进行了详细解释。

该技术的简要总结：Monad（和其他类型类）具有“正常形式”。我们可以将原语（以我们希望的任何方式受到限制）“提升”到这种“规范形式”构造中，它本身就是一种存在数据类型，然后使用我们提升到的类型类可用的任何操作。这些操作本身不受限制，因此我们可以使用 Haskell 的所有普通类型类函数。最后，为了将其转回具体类型（它再次具有我们感兴趣的所有约束），我们“降低”它，这是一个为每个类型类操作采用一个函数的操作，它将在适当的时候应用该函数时间。这样，来自外部的约束（这是提供给降低的函数的一部分）和来自内部的约束（这是我们提升的基元的一部分）就能够匹配，最后我们得到一个大的快乐约束我们可以使用任何普通 Functor/Monoid/Monad 等数据类型。运营。

有趣的是，虽然中间操作不受限制，但据我所知，不可能编写一些“破坏”它们的东西，因为这会破坏所考虑的类型类应遵守的绝对法则。

这可以在constrained-normal Hackage 包中找到，以便在您自己的代码中使用。

我遇到的例子可以按如下方式实现：

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE UndecidableInstances #-}

module Example where

import Data.Dynamic
import Data.Kind
import Data.Typeable

import Control.Monad.ConstrainedNormal


-- | Required to have a simple constraint which we can use as argument to `Expr` / `Expr'`.
-- | This is definitely the part of the example with the roughest edges: I have yet to figure out
-- | how to make Haskell happy with constraints 
class (Show a, Typeable a) => Introspectable a where {}
instance (Show a, Typeable a) => Introspectable a where {}

data Expr' (c :: * -> Constraint) a where
  C :: a -> Expr' c a
  -- M :: (a -> b) -> Expr' a -> Expr' b --^ NOTE: This one is actually never used as ConstrainedNormal will use the 'free' implementation based on A + C.
  A :: c a => Expr' c (a -> b) -> Expr' c a -> Expr' c b


instance Introspectable a => Show (Expr' Introspectable a) where
  show e = case e of
    C x -> "(C " ++ show x ++ ")"
    -- M f x = "(M " ++ show val ++ ")"
    A fx x -> "(A " ++ show (typeOf fx) ++ " " ++ show x ++ ")"

-- | In user-facing code you'd not want to expose the guts of this construction
--   So let's introduce a 'wrapper type' which is what a user would normally interact with.
type Expr c a = NAF c (Expr' c) a

liftExpr :: c a => Expr' c a -> Expr c a
liftExpr expr = liftNAF expr

lowerExpr :: c a => Expr c a -> Expr' c a
lowerExpr lifted_expr = lowerNAF C A lifted_expr

constant :: Introspectable a => a -> Expr c a
constant val = pure val -- liftExpr (C val)

例如，你现在可以写

ghci> val = constant 10 :: Expr Introspectable Int
(C 10)
ghci> (+2) <$> val
(C 12)
ghci> (+) <$> constant 10 <*> constant 32  :: Expr Introspectable Int

通过使用（琐碎约束Data.Constraint.Trivial库的一部分，尽管也可以编写自己的“空约束”），可以改为编写例如

ghci> val = constant 10 :: Expr Unconstrained Int

它将像以前一样工作，但现在val无法打印。

我还没有弄清楚的一件事是如何正确处理约束子集（即，如果我有一个只需要 的函数Show，请使其与 的东西一起工作Introspectable）。目前，一切都必须在“大”约束条件下进行。当然，另一个小缺点是您必须注释约束类型（例如，如果您不需要约束，请Unconstrained手动编写），否则 GHC 会抱怨c0未知。

我们已经达到了这样的目标：拥有一种可以选择性地限制为可打印的类型，所有不需要打印的机器也可以在该类型系列的所有实例上工作，包括那些不可打印的类型，并且该类型可以可以按照您的喜好用作Monoids、Functors、Applicatives 等。

我认为这是一个很好的方法，并想赞扬 Neil Sculthorpe 等人。感谢他们在报纸上所做的工作以及constrained-normal使这一切成为可能的图书馆。太酷了！