haskell - 为什么此约束在这些单独的实例中具有不同的行为？

Question

我做了两种类型的家庭：

{-# Language KindSignatures, DataKinds, TypeOperators, TypeFamilies, FlexibleContexts #-}

import Data.Kind

type family All (c :: Type -> Constraint) (xs :: [Type]) :: Constraint where
  All c '[] = ()
  All c (x ': xs) = (c x, All c xs)

type family Is (f :: Type -> Type) (x :: Type) :: Constraint where
  Is f (f _) = ()

现在我想结合这两个类型族来检查类型级别列表的所有成员是否都是可能的。这是我将如何做到这一点：

All (Is Maybe) tList

现在，如果我尝试使用以下方法对此进行测试：

f :: (All (Is Maybe) '[Maybe Bool]) => a -> a
f = id

我得到一个编译错误：

[1 of 1] Compiling Main             ( familyTest.hs, interpreted )

familyTest.hs:12:6: error:
    • The type family ‘Is’ should have 2 arguments, but has been given 1
    • In the type signature:
        f :: (All (Is Maybe) '[Maybe Bool]) => a -> a
   |
12 | f :: (All (Is Maybe) '[Maybe Bool]) => a -> a
   |      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Failed, no modules loaded.

基于此，我认为我缺少对Is. 我的第一个想法是这与咖喱有关。也许类型族缺乏部分应用。但是，当我去弄清楚我错过了什么时，会发生一些奇怪的事情。首先，我检查所有基本组件的种类：

[1 of 1] Compiling Main             ( familyTest.hs, interpreted )
Ok, one module loaded.
*Main> :k All
All :: (* -> Constraint) -> [*] -> Constraint
*Main> :k Is
Is :: (* -> *) -> * -> Constraint
*Main> :k Maybe
Maybe :: * -> *
*Main> :k Bool
Bool :: *

这里没有任何问题，所以我开始整理：

*Main> :k Is Maybe
Is Maybe :: * -> Constraint

这有点好奇，Is Maybe有种Type -> Constraint。我会预料到这一点，但之前的错误告诉我我将错误数量的参数放入Is. 现在我们尝试将其传递给All：

*Main> :k All (Is Maybe)
All (Is Maybe) :: [*] -> Constraint

令人惊讶的是，这也可以正常工作，即使我们应该期望它。最后要尝试的是完成约束：

*Main> :k All (Is Maybe) '[Maybe Bool]
All (Is Maybe) '[Maybe Bool] :: Constraint

尽管编译器早些时候对这个确切的陈述提出了抱怨，但它仍然有效，但现在这个陈述似乎是一个有效的约束。当我编译原始代码时，我仍然得到同样的错误。

所以此时我开始简化代码，以便隔离行为。

type family App (c :: Type -> Constraint) (x :: Type) :: Constraint where
  App c x = c x

type family IsBool (x :: Type) :: Constraint where
  IsBool Bool = ()

f :: (App IsBool Bool) => a -> a
f = id

这仍然会导致类似的错误：

[1 of 1] Compiling Main             ( familyTest.hs, interpreted )

familyTest.hs:19:6: error:
    • The type family ‘IsBool’ should have 1 argument, but has been given none
    • In the type signature: f :: (App IsBool Bool) => a -> a
   |
19 | f :: (App IsBool Bool) => a -> a
   |      ^^^^^^^^^^^^^^^^^^^^^^^^^^^
Failed, no modules loaded.

当我尝试检查它时，它没有表现出来:k

*Main> :k App IsBool Bool
App IsBool Bool :: Constraint

到底是怎么回事？

标签： haskelltypestype-familiestype-level-computation