封闭式家庭的限制？

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

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

这样

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

所以我们的想法是，任何已经拥有Show实例的东西都可以通过show它变成一个“漂亮”的Text ，除了我们想要特殊情况的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？

---

我觉得由于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 from () 。 换句话说，我们应该能够测试任何给定的类型是否等于Int。 这显然是不可能的。

同样， Show a字典相当于一个函数a -> ShowS 。 你如何能够决定，鉴于此，论证是否是StringLike ？

---

也许我误解了你的目标，但这看起来像是很多工作来获得你想要的类型。

{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, UndecidableInstances, IncoherentInstances #-}
module Prettied where 

import Data.Text (Text, pack)

class Pretty a where pretty :: a -> Text 

instance           Pretty Text   where pretty = id 
instance           Pretty String where pretty = pack 
instance Show a => Pretty a      where pretty = pack . show 

虽然看起来pretty应该有类型Pretty a => a -> Text ，但由于IncoherentInstances它实际上会有类型Show a => a -> Text 。 这应该可能在它自己的模块中，因为启用IncoherentInstances是可以破坏有效代码的那些东西之一。

链接地址: http://www.djcxy.com/p/43135.html

上一篇: Constraints on closed type families?

下一篇: Infer constraints for both if and else of type equality