5

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

这段代码，不包括 function 的定义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 时获得的大部分便利（注入性、生成性等），但我对这种情况下的问题究竟是什么以及如何规避它的理解非常有限. 我可以指定一些可以清除它的约束吗？

4

1 回答 1

2

您应该在这里理解的是，您的代码本身没有任何问题，只是 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函数的类型参数awithSing应该如何实例化。让我在这里重复他的代码以供参考：

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 中仍然缺少对它们的支持或正在进行中。

于 2014-05-26T11:03:39.833 回答