haskell - 隐式参数和类型族

Question

我一直在尝试使用 Data.Singletons 库的依赖类型程序，在论文“使用 Singletons 的依赖类型编程”中开发了长度注释向量之后，我遇到了以下问题。

这段代码，不包括函数indexI的定义，在 GHC 7.6.3 中进行类型检查，并在没有它的情况下按预期工作:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Singletons
import Data.Singletons.TH

data Nat where
  Z :: Nat
  S :: Nat -> Nat
  deriving Eq

$(genSingletons [''Nat])

data FlipList :: * -> * -> Nat -> * where
    Cons :: ((a -> b) -> a -> b) -> FlipList a (a -> b) n -> FlipList a b (S n)
    Nil :: FlipList a b Z

type family (m :: Nat) :< (n :: Nat) :: Bool
type instance m :< Z = 'False
type instance Z :< (S n) = 'True
type instance (S m) :< (S n) = m :< n

type family PreMap a b (m :: Nat) :: *
type instance PreMap a b Z = a -> b
type instance PreMap a b (S n) = PreMap a (a -> b) n

type family BiPreMap a b (m :: Nat) :: *
type instance BiPreMap a b m = PreMap a b m -> PreMap a b m

index :: ((m :< n) ~ 'True) => SNat m -> FlipList a b n -> BiPreMap a b m
index SZ (Cons f _) = f
index (SS sm) (Cons _ fl) = index sm fl

indexI :: ((m :< n) ~ 'True, SingI m) => FlipList a b n -> BiPreMap a b m
indexI = withSing index

包含 indexI 后, GHC 产生两个错误,

Could not deduce (PreMap a b m ~ PreMap a b a0)
    from the context ((m :< n) ~ 'True, SingI Nat m)
      bound by the type signature for
                 indexI :: ((m :< n) ~ 'True, SingI Nat m) =>
                           FlipList a b n -> BiPreMap a b m

和，

Could not deduce (PreMap a b m ~ PreMap a b a0)
    from the context ((m :< n) ~ 'True, SingI Nat m)
      bound by the type signature for
                 indexI :: ((m :< n) ~ 'True, SingI Nat m) =>
                           FlipList a b n -> BiPreMap a b m

这两个错误的根源似乎是术语 withSing index有类型 FlipList a b n -> BiPreMap a b a0 , 并且，无法推导出 a0 ~ m , GHC 无法证明 BiPreMap a b m ~ BiPreMap a b a0 .我知道类型族的类型推断缺乏我们在使用 ADTS 时获得的大部分便利(注入(inject)性、生成性等)，但我对这种情况下的问题究竟是什么以及如何规避它的理解非常有限.我可以指定一些可以清除它的约束吗？

Answer 1

您应该在这里理解的是，您的代码本身没有任何问题，只是 GHC 的类型推断无法确定它的类型安全性。请注意，通过注释掉 indexI ，在 GHC 中加载代码并询问 withSing index 的类型:

*Main Data.Singletons> :t withSing index
  withSing index
    :: (SingI Nat a, (a :< n) ~ 'True) =>
       FlipList a1 b n -> PreMap a1 b a -> PreMap a1 b a

这意味着 GHC 能够对您的代码进行类型检查，它甚至可以推断出与您指定的类型相同的类型(直到 alpha 等效)。那么为什么它不对你的代码进行类型检查呢？

问题是您的代码没有明确说明 withSing 的类型参数如何。应该实例化，特别是类型变量 a应实例化为 m从你的类型签名。可想而知 a应该实例化为其他东西(例如 [m] 或 m -> m )以便您的实现 withSing index具有您指定的类型。 GHC 无法确定 a应实例化为 m ，你得到你得到的错误。请注意，GHC 不会尝试猜测这种实例化，这是一件好事。我们不希望 GHC 的类型级语言退化为 Prolog 解释器；)。在我看来，这已经有点太接近了。

这意味着您有两种选择来解决您的问题。第一种解决方案是上面user2407038提出的:使用类型注解告诉GHC函数 withSing的类型参数a如何应该被实例化。让我在这里重复他的代码以供引用:

indexI :: forall m n a b . ((m :< n) ~ 'True, SingI m) => FlipList a b n -> BiPreMap a b m
indexI = withSing (index :: SNat m -> FlipList a b n -> BiPreMap a b m)

请注意，您需要显式 forall类型签名中的语法以确保 m类型签名在 indexI 的实现范围内(查看有关 GHC 的 ScopedTypeVariables 扩展的文档以获取更多信息)。

您的另一种选择是更改您的代码，以便 GHC 可以确定如何实例化 a通过类型推断。要理解这一点，请考虑 GHC 告诉您它无法推断 PreMap a b m ~ PreMap a b a0 .这意味着 GHC 已经推断出 withSing index到我在这个答案开始时向您展示的类型，并试图找到类型实例以确定此推断类型如何等于您注释的类型。为此，它尝试解决等式约束 BiPreMap a b m ~ BiPreMap a b a0 ，简化为更简单的约束 PreMap a b m ~ PreMap a b a0 .然而，这就是它卡住的地方。因为像 PreMap 这样的类型族不一定是单射的，所以它不能由此决定 m必须等于 a0 .解决此问题的一种方法是更改​​ BiPreMap转换为数据类型或新类型。与类型族不同，数据类型和新类型的参数是单射的，然后 GHC 可以解决约束:

newtype BiPreMap a b m = BiPreMap { getBiPreMap :: PreMap a b m -> PreMap a b m }

index :: ((m :< n) ~ 'True) => SNat m -> FlipList a b n -> BiPreMap a b m
index SZ (Cons f _) = BiPreMap f
index (SS sm) (Cons _ fl) = BiPreMap (getBiPreMap (index sm fl))

indexI :: ((m :< n) ~ 'True, SingI m) => FlipList a b n -> BiPreMap a b m
indexI = withSing index

就是这样，我希望这能澄清一些正在发生的事情......请注意，您尝试执行的“Haskell 中的依赖类型编程”类型在 Haskell 中并不重要，您可能会遇到更多此类一路上的问题。很多时候，显式类型签名将成为您可能遇到的奇怪类型错误的解决方案。显式类型应用程序也很有用，但我知道 GHC 中仍然缺少对它们的支持或正在进行中。