在 Haskell 中的约束内应用约束

Question

无论如何要在另一个约束中应用一个约束，这样

{-# 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.

谢谢！

Answer 1

解决此问题的一种简单方法是使用the LiberalTypeSynonyms extension。此扩展允许 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 知道任何@987654337 的实例@也满足Con'。总的来说，Con 约束在功能上等同于Con'，但可以部分应用。成功！

---

另一方面，GHC proposal for unsaturated type families 最近已被接受，因此在不久的将来可能不需要这些技巧，因为允许部分应用类型族。

Answer 2

Haskell 不支持类型级别的 lambda，也不支持类型族/类型同义词的部分应用。您的Con 必须始终完全应用，不能将未应用的同义词传递给其他类型。

我们最多可以尝试如下使用“去功能化”，有效地为我们需要的类型级 lambdas 命名。

{-# LANGUAGE ConstraintKinds, KindSignatures, TypeFamilies #-}

import Data.Kind

-- Generic application operator
type family Apply f x :: Constraint

-- A name for the type-level lambda we need
data Con
-- How it can be applied
type instance Apply Con x = (Show x, Num x)

-- The wanted type-level function
type App c a b = (Apply c a, Apply c b)

-- Con can now be passed since it's a name, not a function
program :: App Con a b => a -> b -> String
program a b = show a ++ " " ++ show (b+1)

要使用不同的第一个参数调用App，需要重复此技术：定义自定义虚拟类型名称（如Con）并描述如何应用它（使用type instance Apply ... = ...）。