隐式参数和类型族
我一直在使用Data.Singletons库试验依赖类型的程序，在文章“使用Singletons进行依赖类型化编程”之后开发了长度注释向量，并且我遇到了以下问题。
该代码（不包括函数indexI的定义）在GHC 7.6.3中进行了类型indexI ，并在缺少时按预期工作：
{-# 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 abn -> BiPreMap ab a0 ，并且，如果不能够推导出a0 ~ m BiPreMap abm ~ BiPreMap ab a0 ，则GHC无法证明BiPreMap abm ~ BiPreMap ab a0 。 我知道类型系列的类型推断缺乏我们在使用ADTS（注入性，生成性等）时获得的大多数便利，但我对这种情况下的问题以及如何规避它的理解非常有限。 我可以指定哪些限制可以清除它？
你应该在这里理解的是，你的代码没有问题，只是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应该将实例化类型变量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 abm ~ PreMap ab a0 。 这意味着GHC已经根据我在这个答案开始时显示给你的类型推断withSing index ，并试图找到类型实例来确定这个推断类型如何等于你注释的类型。 为此，它试图解决一个等式约束BiPreMap abm ~ BiPreMap ab a0 ，它被简化为一个更简单的约束PreMap abm ~ PreMap ab 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对它们的支持仍然缺失或正在进行。
链接地址: http://www.djcxy.com/p/78249.html