haskell - 高阶列表和类型族的歧义错误

Question

我有一个高阶列表 GADT 定义如下:

data HList as where
    HNil :: HList '[]
    HCons :: a -> HList as -> HList (a ': as)

我可以编写一个函数，让我从该列表中获取第一项，前提是它是非空的:

first :: HList (a ': as) -> HList '[a]
first (HCons a _) = HCons a HNil

但是，如果我创建一个新类型 Cat 和一个仅将类型级别列表中的每个类型应用于 Cat 的类型族(有点像类型级别 map ):

newtype Cat a = Cat a

type family MapCat (as :: [*]) :: [*] where
    MapCat '[] = '[]
    MapCat (a ': as) = Cat a ': MapCat as

还有一个类型 CatList，它将类型列表转换为 HList，其中包含应用于 Cat 的那些类型:

type CatList cs = HList (MapCat cs)

我无法编写适用于 CatList 的类似函数。

first' :: CatList (a ': as) -> CatList '[a]
first' (HCons a _) = HCons a HNil

它出错了:

Couldn't match type ‘MapCat as0’ with ‘MapCat as’
NB: ‘MapCat’ is a type function, and may not be injective
The type variable ‘as0’ is ambiguous
Expected type: CatList (a : as) -> CatList '[a]
  Actual type: CatList (a : as0) -> CatList '[a]
In the ambiguity check for:
  forall a (as :: [*]). CatList (a : as) -> CatList '[a]
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature:
  Testing.fst :: CatList (a : as) -> CatList '[a]

怎么了？ Here is a gist with the entire code .

Answer 1

让我们从一个更简单的例子开始:

type family F a

err :: F a -> ()
err _ = ()

抛出

Couldn't match type ‘F a0’ with ‘F a’ NB:
F is a type function, and may not be injective
The type variable a0 is ambiguous
Expected type: F a -> ()
  Actual type: F a0 -> () …

虽然编译正常:

ok :: (a ~ Int) => F a -> ()
ok _ = ()

还有这个:

type family F a where
    F a = a

ok :: F a -> ()
ok _ = ()

这是另一个例子，更接近你的问题:

data D = C

data Id (d :: D) where
    Id :: Id d

type family TF_Id (d :: D) :: D where
    TF_Id C = C

err :: Id (TF_Id d) -> ()
err _ = ()

错误是

Couldn't match type ‘TF_Id d0’ with ‘TF_Id d’ NB:
TF_Id is a type function, and may not be injective
The type variable d0 is ambiguous
Expected type: Id (TF_Id d) -> ()
  Actual type: Id (TF_Id d0) -> () …

但这行得通:

ok :: Id (TF_Id C) -> ()
ok _ = ()

还有这个:

type family TF_Id (d :: D) :: D where
    TF_Id x = x

ok :: Id (TF_Id d) -> ()
ok _ = ()

因为 TF_Id a 在这两种情况下都会立即减少到 a。

因此，编译器每次无法减少 SomeTypeFamily a 时都会抛出错误，其中 a 是某个类型变量，之前未确定。

所以如果我们想解决这个问题:

type family TF_Id (d :: D) :: D where
    TF_Id C = C

err :: Id (TF_Id d) -> ()
err _ = ()

在不重新定义类型族的情况下，我们需要确定err 类型签名中的d。最简单的方法是

type family TF_Id (d :: D) :: D where
    TF_Id C = C

ok :: Id d -> Id (TF_Id d) -> ()
ok _ _ = ()

或者我们可以为此定义一个数据类型:

data Proxy (d :: D) = Proxy

ok :: Proxy d -> Id (TF_Id d) -> ()
ok _ _ = ()

现在回到 first' 函数:

data Proxy (a :: [*]) = Proxy

first' :: Proxy (a ': as) -> CatList (a ': as) -> CatList '[a]
first' _ (HCons a _) = HCons a HNil

这编译得很好。你可以像这样使用它:

main = print $ first' (Proxy :: Proxy '[Int, Bool]) (HCons (Cat 3) $ HCons (Cat True) HNil)

打印 Cat3:[]。

但编译器唯一必须知道的要减少 MapCat as 的是 as 的弱头部范式，所以我们实际上不需要提供这些额外的类型信息在 Proxy::Proxy '[Int, Bool] 中。这是一个更好的方法:

data ListWHNF (as :: [*]) where
    LZ :: ListWHNF '[]
    LS :: ListWHNF as -> ListWHNF (a ': as)

first' :: ListWHNF (a ': as) -> CatList (a ': as) -> CatList '[a]
first' _ (HCons a _) = HCons a HNil

main = print $ first' (LS $ LS LZ) (HCons (Cat 3) $ HCons (Cat True) HNil)

所以 first' 现在收到一些东西，看起来像列表的长度。但是我们可以静态地做到这一点吗？没那么快:

data ListWHNF (as :: [*]) where
    LZ :: ListWHNF '[]
    LS :: ListWHNF as -> ListWHNF (a ': as)

data HList as ln where
    HNil  :: HList '[] LZ
    HCons :: a -> HList as ln -> HList (a ': as) (LS ln)

throws 数据构造函数 LZ 来自不可提升的类型 ListWHNF ...。我们不能在 Haskell 中使用索引数据类型作为索引。

具有某种功能依赖性，这将允许将一种类型的术语与另一种术语的弱头部范式联系起来，我们可能可以做到这一点，但我不知道 GHC 中有类似的东西(但我不是专家)。在 Agda 中，这很简单

_^_ : ∀ {α} -> Set α -> ℕ -> Set α
A ^ 0     = Lift ⊤
A ^ suc n = A × A ^ n

因此，如果我们唯一需要推断列表的是它的长度，那么我们可以用 n 嵌套元组替换列表。滥用符号，[?, ?]::[*] 变成 (?::*, (?::*, Lift ⊤)) 和所有这些 ? 现在可以自动推断出 ⊤ 的成员(Agda 的 () 等价物)。但是在 Agda 中，没有值级和类型级编程的区别，所以根本不存在这样的问题。