Evg*_*Evg 4 haskell type-families
我想根据第一个参数的类型指定函数结果类型。\n为了定义这种依赖性，我定义了类型族 MaybeWrapper。\n如果第一个参数是 Opt 类型（可选），它会将一些结果类型包装在 Maybe 中。\nOpt 和 Req 是一个单例\n我希望他们定义结果类型Opt -> Maybe v和Req -> v
\n这里是代码：
\n{-# LANGUAGE TypeFamilies #-}\n{-# LANGUAGE TypeApplications #-}\n{-# LANGUAGE ScopedTypeVariables #-}\n\nimport Data.Typeable\nimport Data.Type.Equality\n\n-- singelton types:\ndata Opt = Opt deriving Show\ndata Req = Req deriving Show\n\ntype family MaybeWrapper a v where\n MaybeWrapper Opt v = Maybe v\n MaybeWrapper _ v = v\n\n\nf1 :: forall a v.Typeable a => a -> v -> MaybeWrapper a v\nf1 a vv \n | Just Refl <- eqT @a @Opt = Just vv\n | otherwise = vv\n\nf2 :: a -> v -> MaybeWrapper a v\nf2 Opt vv = Just vv\nf2 _ vv = vv\n但我的所有尝试 1 和 2 都失败了。
\n错误：
\n\xe2\x80\xa2 无法匹配预期类型 \xe2\x80\x98MaybeWrapper av\xe2\x80\x99\n 与实际类型 \xe2\x80\x98v\xe2\x80\x99
\n我希望“MaybeWrapper a v”不是类型，而是必须解析为v 的类型函数类型，并且类型必须匹配。
\n我怎样才能解决这个问题？
\n添加：
\n所以我发现我可以用类型类修复它：
\nclass CMaybe a where\n type MWrap a v \n vf :: a -> v -> MWrap a v \n\ninstance CMaybe Opt where\n type MWrap Opt v = Maybe v\n vf _ = Just \n\ninstance CMaybe Req where\n type MWrap Req v = v\n vf _ v = v\n但为什么如果没有它们，haskell 就无法推断类型呢？
\n首先，你的第二次尝试是完全不可能的。您根本无法匹配类型仅为变量的值，例如a与一种特定类型的模式（例如Opt，这是名为 的类型的模式Opt）。Stack Overflow 上有很多问题和答案，更详细地讨论了这个问题，所以我不会在这里详细说明。
您的第一次尝试更有趣，所以让我们考虑一下为什么它不起作用。
\n首先，我希望这不起作用的原因很明显：
\nf1 :: forall a v.Typeable a => a -> v -> MaybeWrapper a v\nf1 a vv = vv\nvv编译右侧的表达式时，编译器没有关于类型a是什么（或v与此相关的信息）的信息。因此，当它查看 的定义时MaybeWrapper a v，它没有任何证据，a因此Opt无法采用第一个分支并得出结论MaybeWrapper a v = Maybe v。但它也没有任何证据证明a不是； 所以它也Opt不能采用第二个分支。
剩下的就是右侧的类型应该是 simple MaybeWrapper a v；如果没有任何信息，它无法将类型族缩减为任何特定类型。这就是为什么你会收到如下错误：
\xe2\x80\xa2 Couldn't match expected type \xe2\x80\x98MaybeWrapper a v\xe2\x80\x99\n with actual type \xe2\x80\x98v\xe2\x80\x99\n这并不是说这MaybeWrapper a v是某种具体类型，而是说它不知道计算结果是什么具体类型，因此它无法与其他任何类型相匹配。
（如果f1采用具有 type 的参数MaybeWrapper a v，则可以得出结论，参数值与返回值具有相同的类型，因此即使不减少类型族，您也可以返回该值。但是您实际上无法做任何其他事情其值的类型是未约简类型族）
那么我们可以看看你的实际情况f1：
f1 :: forall a v.Typeable a => a -> v -> MaybeWrapper a v\nf1 a vv \n | Just Refl <- eqT @a @Opt = Just vv\n | otherwise = vv\n在第一个分支中，您使用Typeable和eqT。这允许您编写代码的特定分支，编译器认为它有证据表明a ~ Opt. 这意味着它可以减少MaybeWrapper a v到Maybe v，因此您可以返回Just vv该分支。如果您仔细查看收到的错误消息，您会发现它并不是在抱怨这一行；而是在抱怨这一行。编译器在这里很高兴。
但附加证据仅适用于模式匹配的范围内Just Refl。在模式匹配之外，所有代码都必须在完全缺乏有关类型的任何信息的情况下进行编译a。您可能希望处于只有在eqT匹配失败时才能到达的分支中，以便为编译器提供类型不等式的证据，但这根本不是它的工作原理。
（当eqT测试类型并发现它们相等时，它会返回Just Refl，其中Refl是一个特殊值，为编译器提供类型相等的证据。但是当eqT发现类型不相等时，它只会返回Nothing，这并不不包含类型检查器可以使用的任何证据；并且您甚至没有对其进行模式匹配，因此即使证据存在，您也不会获得证据）。
因此，您可以通过再次使用来使代码正常eqT工作：
f1 :: forall a v.Typeable a => a -> v -> MaybeWrapper a v\nf1 a vv \n | Just Refl <- eqT @a @Opt = Just vv\n | Just Refl <- eqT @a @Req = vv\n现在，您的两个分支都已使用有关a. 知道aisReq就足以减少MaybeWrapper a v到v，因此在该分支上您可以vv根据需要返回。
这样做的问题是，现在你的守卫并不详尽（如果你使用，编译器会警告你-Wall）。您知道您希望此参数为Optor Req，但您实际上所说的是它可以是具有实例的任何类型。尝试编写一个文件，其中您可以将其称为, 或; 类型检查器会很高兴地允许它，但是运行该代码将在运行时失败。所以这不是很类型安全的。aTypeablef1 True ()f1 (putStrLn "whoops") ()Non-exhaustive patterns in function f1
更好的方法是将Opt和Req 一起定义为新类型的唯一可能的成员，而不是将它们定义为单独的类型。然后，您可以定义一个单例 GADT，它提供对值进行模式匹配的能力，以查明类型参数是否是Optor Req（并不允许任何其他类型）。通过这种设置，您所需要的只是常规模式匹配来完成您想要的操作；无Typeable或自定义类型类。它看起来像这样（使用 GHC 9.4.8 按原样编译；您可能需要在旧版本中启用更多扩展）：
{-# LANGUAGE DataKinds #-}\n{-# LANGUAGE TypeFamilies #-}\n\nimport Data.Kind ( Type )\n\n\n-- Optionality is an ordinary type, with Opt and Req as value\n-- constructors. We're never going to use it like that, however. The\n-- DataKinds extension will automatically allow us to use Opt and Req\n-- as (uninhabited) types, with Optionality being a *kind* that allows\n-- only those two types (a kind is a "type of types").\ndata Optionality = Opt | Req\n\n-- Because the Opt and Req *types* are uninhabited, we need something\n-- else we can pass as the first argument to our function. Note that\n-- the separate type signature for the data type is called\n-- "stand-alone kind signature"; this is relatively new syntax but\n-- makes things a lot clearer.\ntype OptionalitySingleton :: Optionality -> Type\ndata OptionalitySingleton a where\n SingletonForOpt :: OptionalitySingleton Opt\n SingletonForReq :: OptionalitySingleton Req\n\n-- Again I've provided a stand-alone kind signature to make it clear\n-- what kinds of type MaybeWrapper works with.\ntype MaybeWrapper :: Optionality -> Type -> Type\ntype family MaybeWrapper o v where\n MaybeWrapper Opt v = Maybe v\n MaybeWrapper Req v = v\n\n-- Finally, f itself is almost trivial\nf :: OptionalitySingleton a -> v -> MaybeWrapper a v\nf SingletonForOpt vv = Just vv\nf SingletonForReq vv = vv\n（请注意，为了使示例清晰，我使用了令人烦恼的长名称；通常在应用此模式时，人们使用更短的名称；Sing或者S前缀/后缀很常见）
您可能想知道为什么不能只使用OptandReq作为f;的第一个参数。为什么我要搞乱整个单独的OptionalitySingleton类型？但是如果我们使用值级别Opt，那么该参数的类型Req必须是Optionalityf必须如下所示：
f :: Optionality -> v -> MaybeWrapper a v\n这里的ainMaybeWrapper a v与第一个参数完全无关Optionality，因此我们不会a通过Optionality值的模式匹配来了解任何信息。并且 type 中没有变量Optionality，因此我们无法连接到任何内容a任何内容。
而类型级别Opt和Req根本没有任何值（只有 kind 中的类型Type才有值；类型级别Opt和则Req在 kind 中Optionality），所以我们没有任何东西可以传递给f. 即使我们可以，他们还是不同的类型，因此当我们还不知道类型参数是什么时，没有可以使用的模式对它们都有效。
因此，我们必须定义一个单独的类型，例如OptionalitySingleton（使用where语法定义类型的功能称为GADT或广义代数数据类型语法的功能，如果您还没有见过它并且想通过 google 搜索更多信息）。此模式采用类型参数，然后定义类型，以便类型参数的每个值只有一个可能的构造函数（因此称为“单例”，与面向对象编程中的术语“单例”完全无关）。这意味着构造函数上的模式匹配完全标识了类型参数必须是什么，并且编译器内置了特殊支持，可以利用 GADT 上的模式匹配获得的证据。
因此f可以继续对OptionalitySingleton值进行模式匹配，然后在每个分支中使用不同的返回类型。与上面的两个eqT分支一样，您仍然需要明确在每个分支中匹配的类型。没有办法使用_orotherwise和 拥有一个包罗万象的分支，因为我们仍然只能编写具有类型相等的积极证据的分支，我们不能编写具有类型不平等的可用证据的分支。但现在我们对其进行了限制，以便唯一可能的类型是Optand Req（或者更确切地说，唯一可能的值是SingletonForOptand SingletonForReq）；-Wall如果我们忘记处理所有情况，编译器会警告我们（使用）（当您稍后将 扩展Optionality为具有第三种可能性并需要更新模式匹配的每个位置时非常有用），并且实际上还会警告我们我们添加了另一种情况f（编译器会注意到它一定是多余的，因为我们已经匹配了所有可能匹配的内容）。
| 归档时间： |
|
| 查看次数： |
105 次 |
| 最近记录： |