在运行时检查约束

Question

我正在尝试定义一个函数，该函数检测输入的类型是否满足给定的约束：

satisfies :: (c a => a -> b) -> a -> Maybe b
-- or the more general
claim :: (c => a) -> Maybe a

因此，所需的行为将是：

>>> :t satisfies @Show show
satisfies @Show show :: a -> Maybe String
>>> satisfies @Show show (0 :: Int)
Just "0"
>>> satisfies @Show show (id :: Int -> Int)
Nothing

目标是使定义完全多态功能变得容易尽可能的专业优势：

showAny :: a -> String
showAny (satisfies @Show show -> Just str) = str
showAny (satisfies @Typeable showType -> Just str) = "_ :: " ++ str
showAny _ = "_"

作为我可以尝试的最简单的事情，我第一次尝试使用-fdefer-to-runtime

尝试

{-# OPTIONS_GHC -fdefer-type-errors -Wno-deferred-type-errors #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE RankNTypes #-}
module Claim where
import System.IO.Unsafe (unsafePerformIO)
import System.IO.Error (catchIOError)
satisfies :: (c a => a -> b) -> a -> Maybe b
satisfies f a = unsafePerformIO $
  (return . Just $! f a) `catchIOError` _ -> return Nothing

这失败了，因为-fdefer-type-errors没有将检查推迟到运行时，或允许在上下文中进行进一步检查实际使用(如我所希望的(，但在编译时间替换时已找到与error "MESSAGE"的等效键入错误。

现在我没有想法了。是否可能实现satisfies？

Answer 1

您无法在运行时派遣实例可用性。请记住，编译器将约束转换为A 类型类词典 - 在运行时明确并明确访问的功能记录。" fat Arrow" =>在运行时用"薄箭头" ->表示，因此示出者需要在编译时知道哪个字典要传递。

也就是说，以下粗糙示例：

class Show a where
    show :: a -> String
instance Show String where
    show = id
showTwice :: Show a => a -> String
showTwice x = show x ++ show x
main = putStrLn $ showTwice "foo"

生成核心代码，看起来大致喜欢：

data Show_ a = Show_ { show :: a -> String }
showString_ :: Show_ String
showString_ = Show_ { show = id }
showTwice :: Show_ a -> a -> String
showTwice show_ x = show show_ x ++ show show_ x
main = putStrLn $ showTwice showString_ "foo"

在为main生成代码时，编译器需要知道在哪里找到showString_。

您可以想象一个系统，可以通过某种内省机制在运行时查找类型类词典，但这将从语言设计的角度产生怪异的行为。问题是孤儿实例。如果我编写了一个尝试在模块A中查找给定实例的函数，并在无关的模块B中定义了该实例，那么当从某些客户端模块C调用时，该函数的行为取决于B是否由其他某些其他某些导入程序的一部分。很奇怪！

---

执行"完全多态函数，可以在可能的情况下优势"的一种更常见的方法是将所讨论的函数放入类型类本身中，并为其提供默认实现(如果默认实现，则使用default签名取决于一些超类(。然后，您的showAny看起来像这样：

{-# LANGUAGE DefaultSignatures #-}
import Data.Typeable
class ShowAny a where
    showAny :: a -> String
    default showAny :: Typeable a => a -> String
    showAny x = "_ :: " ++ show (typeOf x)

您需要为要使用showAny的所有类型实现ShowAny，但这通常是一行代码，

instance (Typeable a, Typeable b) => ShowAny (a -> b)

，您可以通过覆盖showAny来专门针对给定类型的实现。

instance ShowAny String where
    showAny = id

您在执行通用编程的库中经常看到这种方法。例如，aeson可以使用GHC.Generics来序列化JSON的给定类型(您要做的就是派生Generic并写两行instance ToJSON MyType; instance FromJSON MyType(，但是您也可以编写自己的ToJSON和FromJSON的实例'T足够快，或者您需要自定义输出。

Answer 2

可接受的答案的替代解决方法是手动通过词典。

，即：

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
module Claim where
data Proof c where QED :: c => Proof c
type Claim c = Maybe (Proof c)
type c ? a = Maybe (Proof (c a))

一个人可以写：

showAny :: (Show? a, Typeable? a) -> a -> String
showAny (Just QED, _) a = show a
showAny (_, Just QED) a = "_ :: " ++ showType a
showAny _ _ = "_"

效果很好：

>>> showAny (Nothing, Just QED) (id :: Int -> Int)
"_ :: Int -> Int"
>>> showAny (Just QED, Just QED) (0 :: Int)
"0"
>>> showAny (Nothing, Nothing) undefined
"_"