如何仅以一种方式揭露强制行为？

Question

考虑一下这个有点愚蠢的数据类型：

type data AllowPrimesOnly = PrimesOnly | AllNumbers

data Number (allowPrimesOnly :: AllowPrimesOnly) where
  One :: Number AllNumbers
  Two :: Number allowPrimesOnly
  Three :: Number allowPrimesOnly
  Four :: Number AllNumbers
  Five :: Number allowPrimesOnly

有了这个定义，我就可以定义：

f :: Number allowPrimesOnly -> Int
f = \case
  One -> 1
  Two -> 2
  Three -> 3
  Four -> 4
  Five -> 5

fPrime :: Number PrimesOnly -> Int
fPrime = \case
  Two -> 2
  Three -> 3
  Five -> 5

很高兴，GHC 会适当地发出警告（或不发出警告）。

特别注意

f

，它适用于两种类型。也许将

f

应用于

Number PrimeOnly

会效率低下，因为它正在检查从未存在的分支，但它仍然有效。

但是当我尝试这样做时：

g :: Number PrimesOnly -> Number AllNumbers
g = coerce

我遇到问题了。我无法在不同的

coerce

类型之间进行

Number

，因为

allowPrimesOnly

的角色是

nominal

，因为

Number

是 GADT。

现在让我们说我这样定义

Number

：

data Number (allowPrimesOnly :: AllowPrimesOnly) = One | Two | Three | Four | Five

现在：

g :: Number PrimesOnly -> Number AllNumbers
g = coerce

确实有效。但我们现在收到了

fPrime

的警告。不过，我们可以通过一些技巧来解决这个问题：

view :: Number PrimesOnly -> Maybe Void
view = const Nothing 

pattern MatchPrimesOnly :: Void -> Number PrimesOnly
pattern MatchPrimesOnly x <- (view -> Just x)

{-# COMPLETE Two, Three, Five, MatchPrimesOnly #-}

fPrime :: Number PrimesOnly -> Int
fPrime = \case
  Two -> 2
  Three -> 3
  Five -> 5
  MatchPrimesOnly x -> Void.absurd x

MatchPrimesOnly

模式有点像黑客，强制完整的编译指示仅适用于

Number PrimesOnly

。

到目前为止一切顺利。我们必须添加一些技巧，让编译器在我们仅对素数进行模式匹配时不发出警告（因为仅使用

{-# COMPLETE Two, Three, Five #-}

会允许与

Number AllNumbers

进行不完整的匹配），但我们有现在有问题：

g2 :: Number AllNumbers -> Number PrimesOnly
g2 = coerce

有效。但它不应该。请注意，我们需要以下内容：

thisShouldCompile :: Number PrimesOnly -> Number AllNumbers
thisShouldCompile = coerce

thisShouldCompileAsWell :: [Number PrimesOnly] -> [Number AllNumbers]
thisShouldCompileAsWell = coerce

butThisShouldFailToCompile :: Number AllNumbers -> Number PrimesOnly
butThisShouldFailToCompile = coerce

我不只是想写：

doCoerce :: Number PrimesOnly -> Number AllNumbers
doCoerce = coerce

并将其公开为函数，因为那样我还必须编写，

doCoerceHigher :: f (Number PrimesOnly) -> f (Number AllNumbers)
doCoerceHigher = coerce

因为我什至不知道如何写这个，甚至这也没有涵盖

coerce

可以使用的所有可能性。

有什么方法可以实现我在这里想要实现的目标吗？

Answer 1

根据您的第一个想法，我们可以将素数类型定义为

forall a. Number a

:

type Prime = forall a. Number a

primeToPrime :: Prime -> Number PrimesOnly
primeToPrime n = n

primeToNumber :: Prime -> Number AllNumbers
primeToNumber n = n

直观地说，

Number

是

AllowPrimesOnly

之上的类型族，如下所示：

                      1
2 ━━━━━━━━━━━━━━━━━━━ 2
3 ━━━━━━━━━━━━━━━━━━━ 3
                      4
5 ━━━━━━━━━━━━━━━━━━━ 5
_______________________
PrimesOnly | AllNumbers

类型

forall a. Number a

是该类型族的“全局部分”的类型：上图中的水平线。评估

AllNumbers

处的全局部分给出

Number AllNumbers

的相应元素。

理想情况下，我们希望将

AllowPrimesOnly

视为一种“有向区间”

PrimesOnly → AllNumbers

，这样我们就可以从

PrimesOnly

强制到

AllNumbers

（或任意点

a

），但不能强制反过来说。请参阅此博文了解相关想法。然而，我认为 GHC 的类型系统不足以表达这一点。

这也让我想起了 Alexis King 的

MonoMaybe

类型族，它使用类似的思想来表达“单调递增”函数

Maybe a -> Maybe b

。我不久前在这里问过这个问题。