在Haskell中的约束内应用约束
无论如何要在另一个约束中应用一个约束，使得这个
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE KindSignatures #-}
module Test where
type Con a = (Num a, Show a)
type App c a b = (c a, c b)
program :: App Con a b => a -> b -> String
program a b = show a ++ " " ++ show (b+1)
将工作？
目前 GHC 给了我以下错误：
[1 of 1] Compiling Test ( Test.hs, interpreted )
Test.hs:9:12: error:
• Expected a constraint, but ‘App Con a b’ has kind ‘*’
• In the type signature: program :: App Con a b => a -> b -> String
|
9 | program :: App Con a b => a -> b -> String
| ^^^^^^^^^^^
Test.hs:9:16: error:
• Expected kind ‘* -> *’, but ‘Con’ has kind ‘* -> Constraint’
• In the first argument of ‘App’, namely ‘Con’
In the type signature: program :: App Con a b => a -> b -> String
|
9 | program :: App Con a b => a -> b -> String
| ^^^
Failed, no modules loaded.
谢谢！
回答
一个简单的方法来解决，这是使用的LiberalTypeSynonyms扩展。此扩展允许 GHC 首先将类型同义词视为替换，然后才检查同义词是否已完全应用。请注意，GHC 在种类推断方面可能有点愚蠢，因此您需要非常清楚它（即显式签名）。尝试这个：
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LiberalTypeSynonyms #-}
module Test where
import Data.Kind (Constraint)
type Con a = (Num a, Show a)
type App c a b = (c a, c b) :: Constraint
program :: App Con a b => a -> b -> String
program a b = show a ++ " " ++ show (b+1)
在我明白这可以用 解决之前LiberalTypeSynonyms，我有一个不同的解决方案，我会保留在这里以防有人感兴趣。
尽管您收到的错误消息有点误导，但您代码的根本问题归结为 GHC 不支持部分应用类型同义词，您在App Con a b. 有几种方法可以解决这个问题，但我发现最简单的方法是按照以下模式将类型同义词约束转换为类约束：
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
type Con' a = (Num a, Show a)
class Con' a => Con a
instance Con' a => Con a
你可以在Con任何你打算使用旧定义的地方使用这个定义。
如果您对它的工作方式/原因感兴趣，这基本上是一个技巧，可以解决 GHC 缺乏对部分类型同义词/系列应用程序的支持，适用于这些类型同义词/系列定义简单约束的特定情况。
我们正在做的是定义一个类，每个类都有一个同名的约束。现在，请注意该类没有主体，但关键的是，该类本身有一个约束（在上述情况下Con' a），这意味着该类的每个实例都必须具有相同的约束。
接下来，我们创建了一个令人难以置信的泛型实例Con，只要约束Con'保持在该类型上，它就可以覆盖任何类型。从本质上讲，这确保了作为 的实例的任何类型Con'也是 的实例Con，并且Con'对Con类实例的约束确保 GHC 知道作为 的实例的任何东西Con也满足Con'。总的来说，Con约束在功能上等效于Con'，但可以部分应用。成功！
另一方面，GHC 对不饱和类型家族的提议最近被接受了，所以在不久的将来，这些技巧可能是不必要的，因为类型家族的部分应用变得允许。
- Your "silly" trick is not at all silly. In a number of situations, it's really the only way to go.