隐式参数和类型系列

Question

我一直在使用Data.Singletons库试验依赖类型的程序,继本文中的长度注释向量的开发,"依赖于单例类型编程",我遇到了以下问题.

此代码,不包括函数的定义,indexIGHC 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时所获得的大部分便利(注入,生成等),但我对这种情况下究竟是什么问题以及如何规避它的理解非常有限.我可以指定哪些约束可以清除它吗？

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