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

Question

在 Haskell 中，id函数在类型级别上定义为，id :: a -> a并实现为仅返回其参数而不进行任何修改，但如果我们进行一些类型自省，TypeApplications我们可以尝试在不破坏类型签名的情况下修改值：

\n

{-# LANGUAGE AllowAmbiguousTypes, ScopedTypeVariables, TypeApplications #-}\n\nmodule Main where\n\nclass TypeOf a where\n  typeOf :: String\n\ninstance TypeOf Bool where\n  typeOf = "Bool"\n\ninstance TypeOf Char where\n  typeOf = "Char"  \n\ninstance TypeOf Int where\n  typeOf = "Int"  \n   \ntweakId :: forall a. TypeOf a => a -> a\ntweakId x \n  | typeOf @a == "Bool" = not x\n  | typeOf @a == "Int" = x+1\n  | typeOf @a == "Char" = x\n  | otherwise = x\n

\n

这会失败并出现错误：

\n

\n

“无法将预期类型 \xe2\x80\x98a\xe2\x80\x99 与实际类型 \xe2\x80\x98Bool\xe2\x80\x99 匹配”

\n

\n

但我在这里没有看到任何问题（类型签名满意）：

\n

我的问题是：

\n

\n
1. 我们怎样才能在 Haskell 中做这样的事情呢？
\n
2. 如果我们不能，那是理论\哲学等原因吗？
\n
3. 如果tweak_id的这个实现不是“原始id”，那么该id函数不得在术语级别进行任何修改的理论根源是什么。或者我们可以有许多函数的id :: a -> a实现（我发现在实践中我们可以，例如我可以在 Python 中实现这样的函数，但是 Haskell 背后的理论对此有何评论？）
\n

\n

Answer 1

为此，您需要 GADT。

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

import Data.Typeable
import Data.Type.Equality

tweakId :: forall a. Typeable a => a -> a
tweakId x
  | Just Refl <- eqT @a @Int = x + 1
  -- etc. etc.
  | otherwise                = x

这里我们用来eqT @type1 @type2检查两个类型是否相等。如果是，结果是Just Refl并且模式匹配足以Refl让类型检查器相信这两种类型确实相等，因此我们可以使用x + 1sincex现在不仅是type a，而且是type Int。

此检查需要运行时类型信息，但由于 Haskell 的类型擦除属性，我们通常没有这些信息。该信息由类型类提供Typeable。

TypeOf如果我们让它提供自定义 GADT 值，也可以使用像您这样的用户定义类来实现。如果我们想要编码一些约束，例如“类型a是 an Int、 aBool或 a String”，其中我们静态地知道允许哪些类型（我们甚至可以以这种方式递归地定义一组允许的类型），那么这可以很好地工作。然而，为了允许任何类型，包括尚未定义的类型，我们需要类似Typeable. 这也非常方便，因为任何用户定义的类型都会自动成为 的实例Typeable。

Answer 2

\n

此失败并出现错误：“无法将预期类型 \xe2\x80\x98a\xe2\x80\x99 与实际类型 \xe2\x80\x98Bool\xe2\x80\x99 匹配”
但我没有看到任何问题这里

\n

\n

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

\n

instance TypeOf Float where\n  typeOf = "Bool"\n

\n

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

\n

你可以确信没有人会通过使用不安全的强制来添加恶意实例，则

\n

import Unsafe.Coerce\n\ntweakId :: forall a. TypeOf a => a -> a\ntweakId x \n  | typeOf @a == "Bool" = unsafeCoerce (not $ unsafeCoerce x)\n  | typeOf @a == "Int" = unsafeCoerce (unsafeCoerce x+1 :: Int)\n  | typeOf @a == "Char" = unsafeCoerce (unsafeCoerce x :: Char)\n  | otherwise = x\n

\n

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

\n

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

\n

{-# LANGUAGE DataKinds, FunctionalDependencies\n           , ScopedTypeVariables, UnicodeSyntax, TypeApplications #-}\n\nimport GHC.TypeLits (KnownSymbol, symbolVal)\nimport Data.Proxy (Proxy(..))\nimport Unsafe.Coerce\n\nclass KnownSymbol t => TypeOf a t | a->t, t->a\n\ninstance TypeOf Bool "Bool"\ninstance TypeOf Int "Int"\n\ntweakId :: \xe2\x88\x80 a t . TypeOf a t => a -> a\ntweakId x = case symbolVal @t Proxy of\n  "Bool" -> unsafeCoerce (not $ unsafeCoerce x)\n  "Int" -> unsafeCoerce (unsafeCoerce x + 1 :: Int)\n  _ -> x\n

\n

诀窍在于，fundept->a使编写另一个实例如

\n

instance TypeOf Float "Bool"\n

\n

那里出现编译错误。

\n

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

\n

class Tweakable a where\n  tweak :: a -> a\n\ninstance Tweakable Bool where\n  tweak = not\ninstance Tweakable Int where\n  tweak = (+1)\ninstance Tweakable Char where\n  tweak = id\n

\n