在密闭型家庭约束？

Question

我想写类型的函数的一个可怕的非参数版

pretty :: (Show a) => a -> Text

这样的

pretty :: Text -> Text = id
pretty :: String -> Text = T.pack
pretty :: (Show a) => a -> Text = T.pack . show

这样的想法是,已经有一个什么Show情况下可以变成一个"漂亮" Text的只是show-ing它,除了Text和String我们希望的特殊情况.

以下代码有效:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE DataKinds, ConstraintKinds #-}
module Pretty (pretty) where

import Data.Text (Text)
import qualified Data.Text as T

type family StringLike a :: Bool where
    StringLike String = True
    StringLike Text = True
    StringLike a = False

class (b ~ StringLike a) => Pretty' a b where
    pretty' :: a -> Text

instance Pretty' String True where
    pretty' = T.pack

instance Pretty' Text True where
    pretty' = id

instance (Show a, StringLike a ~ False) => Pretty' a False where
    pretty' = T.pack . show

type Pretty a = (Pretty' a (StringLike a))

pretty :: (Pretty a) => a -> Text
pretty = pretty'

并且它可以在不除出口任何使用pretty功能.

不过,我不太高兴的类型签名pretty:

pretty :: (Pretty a) => a -> Text

我觉得既然StringLike是一个密闭型的家庭,应该有一种方式,GHC弄清楚,如果只是(Show a)成立,(Pretty a)是已经满足,因为:

1. The following hold trivially just by substituting the results of applying StringLike:
(StringLike String ~ True, Pretty' String True)
(StringLike Text ~ True, Pretty' Text True)

2. For everything else, we *also* know the result of applying StringLike:
(Show a, StringLike a ~ False) => (Pretty' a (StringLike a))

有没有办法说服这个GHC？

Answer 1

我觉得既然StringLike是一个封闭式的家庭,GHC应该有办法弄清楚,如果只(Show a)持有,(Pretty a)已经满足了

要做到这一点,需要进行类型检查,并且会破坏参数多态性.考虑定义一个类型系列

type family IsInt a :: Bool where
  IsInt Int = True
  IsInt a = False
class (b ~ IsInt a) => TestInt a b where
  isInt :: a -> Bool
instance TestInt Int True where
  isInt _ = True
instance (IsInt a ~ False) => TestInt a False where
  isInt _ = False

现在,通过你的说法,GHC应该能够满足TestInt a从().换句话说,我们应该能够测试任何给定类型是否等于Int.这显然是不可能的.

同样,Show a字典相当于一个函数a -> ShowS.既然如此,你怎么能决定这个论点是StringLike什么？