haskell - 我们可以在 Haskell 中调整 "a -> a"函数吗？

Question

在 Haskell 中，id 函数在类型级别上被定义为 id::a -> a 并且实现为只返回它的参数而不做任何修改，但是如果我们有一些使用 TypeApplications 进行类型自省(introspection)，我们可以尝试在不破坏类型签名的情况下修改值:

{-# LANGUAGE AllowAmbiguousTypes, ScopedTypeVariables, TypeApplications #-}

module Main where

class TypeOf a where
  typeOf :: String

instance TypeOf Bool where
  typeOf = "Bool"

instance TypeOf Char where
  typeOf = "Char"  

instance TypeOf Int where
  typeOf = "Int"  
   
tweakId :: forall a. TypeOf a => a -> a
tweakId x 
  | typeOf @a == "Bool" = not x
  | typeOf @a == "Int" = x+1
  | typeOf @a == "Char" = x
  | otherwise = x

这失败并出现错误:

"Couldn't match expected type ‘a’ with actual type ‘Bool’"

但我在这里没有看到任何问题(类型签名满意):

我的问题是:

1. 我们如何在 Haskell 中做这样的事情？
2. 如果我们不能，这是理论\哲学等方面的原因吗？
3. 如果 tweak_id 的这个实现不是“原始 id”，那么 id 函数不得在术语级别上进行任何修改的理论依据是什么。或者我们可以有许多 id::a -> a 函数的实现(我看到在实践中我们可以，例如我可以在 Python 中实现这样的函数，但是 Haskell 背后的理论对这个？)

Answer 1

This fail with error: "Couldn't match expected type ‘a’ with actual type ‘Bool’"
But I don't see any problems here

好吧，如果我添加这个实例会怎么样:

instance TypeOf Float where
  typeOf = "Bool"

你现在看到问题了吗？没有什么能阻止某人添加这样的实例，无论它多么愚蠢。因此，编译器不可能假设已检查 typeOf @a == "Bool" 足以实际使用 x 作为 Bool 类型。

如果您确信没有人会通过使用不安全的强制转换来添加恶意实例，您可以压制错误。

import Unsafe.Coerce

tweakId :: forall a. TypeOf a => a -> a
tweakId x 
  | typeOf @a == "Bool" = unsafeCoerce (not $ unsafeCoerce x)
  | typeOf @a == "Int" = unsafeCoerce (unsafeCoerce x+1 :: Int)
  | typeOf @a == "Char" = unsafeCoerce (unsafeCoerce x :: Char)
  | otherwise = x

但我不会推荐这个。正确的方法是不要使用字符串作为穷人的类型表示，而是使用标准的 Typeable class它实际上是防篡改的，并带有合适的 GADT，因此您不需要手动进行不安全的强制转换。参见 chi's answer .

作为替代方案，您还可以使用类型级字符串 和函数依赖来使不安全的强制转换安全:

{-# LANGUAGE DataKinds, FunctionalDependencies
           , ScopedTypeVariables, UnicodeSyntax, TypeApplications #-}

import GHC.TypeLits (KnownSymbol, symbolVal)
import Data.Proxy (Proxy(..))
import Unsafe.Coerce

class KnownSymbol t => TypeOf a t | a->t, t->a

instance TypeOf Bool "Bool"
instance TypeOf Int "Int"

tweakId :: ∀ a t . TypeOf a t => a -> a
tweakId x = case symbolVal @t Proxy of
  "Bool" -> unsafeCoerce (not $ unsafeCoerce x)
  "Int" -> unsafeCoerce (unsafeCoerce x + 1 :: Int)
  _ -> x

诀窍在于 fundep t->a 使得编写另一个实例就像

instance TypeOf Float "Bool"

编译错误就在那里。

当然，真正最明智的方法可能是根本不理会任何类型的手动类型相等，而只是立即使用该类来进行您需要的行为更改:

class Tweakable a where
  tweak :: a -> a

instance Tweakable Bool where
  tweak = not
instance Tweakable Int where
  tweak = (+1)
instance Tweakable Char where
  tweak = id