提升类型的模式匹配答案

【问题标题】：Pattern Matching on Promoted Types提升类型的模式匹配
【发布时间】：2014-05-22 15:57:39
【问题描述】：

我们可以为* 类型的参数编写单个综合实例：

class MyClass d where
    f :: d -> Int

instance MyClass (Maybe d) where  
    f _ = 3

test1 :: Maybe d -> Int
test1 x = f x

这编译得很好，请注意我们不需要对 test1 的 (MyClass (Maybe d)) 约束，因为编译器会为任何 Maybe d 找到匹配的实例。

我们甚至可以为类型构造函数的类参数编写一个包罗万象的实例：

class MyClass2 (a :: * -> *) where
    g :: Tagged (a Int) Int

instance MyClass2 a where
    g = Tagged 3

test2 :: Int
test2 = untag (g :: Tagged (Maybe Int) Int)

这也编译得很好，并且 test2 不需要 (MyClass2 Maybe) 约束，因为编译器会找到匹配的实例。

考虑以下玩具代码来计算（提升）类型列表的长度：

{-# LANGUAGE TypeOperators,
DataKinds,
KindSignatures,
GADTs,
FlexibleInstances,
FlexibleContexts,
ScopedTypeVariables #-}

import Data.Tagged
import Data.Proxy

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

class ListLen a where
    len :: Tagged a Int

instance ListLen (HList '[]) where
    len = Tagged 0

instance (ListLen (HList as)) => ListLen (HList (a ': as)) where
    len = Tagged (1+(untag (len :: Tagged (HList as) Int)))

test3 :: Int
test3 = untag (len :: Tagged (HList '[Int, Double, Integer]) Int)

test4 :: (Proxy (HList qs)) -> Int
test4 (_ :: Proxy (HList qs)) = untag (len :: Tagged (HList qs) Int) -- error occurs here

这会导致错误：

No instance for (ListLen (HList qs))
      arising from a use of `len'
    Possible fix: add an instance declaration for (ListLen (HList qs))
    ...

如果我们注释掉test4 的签名，GHCi 将类型推断为

test4 :: (ListLen (HList qs)) => (Proxy (HList qs)) -> Int

但这不应该是必要的。显然，我已经为ListLen 编写了匹配任何可能的类型列表的实例：一个“空列表”案例和一个“缺点”案例。如果我将ListLen 参数的类型更改为[*] 类型（即删除ListLen 及其实例中的HList 包装器），问题仍然存在。

如果我们注释掉test4，test3 编译并运行良好：因为我（基本上）为我如何构造类型列表提供了明确的语法（'[Int,Double,Integer]），编译器能够找到匹配的实例。

我正在尝试编写为我构建类型列表的代码，因此我不必写出显式类型列表语法。然而，使用显式语法似乎是 GHC 能够匹配这些综合实例的唯一方法。也许我错过了一个案例？我没有使用的语法？

我可以做些什么来让 GHC 意识到我有一个实例来处理 [*][*]? 我正在使用 GHC 7.4.2。这可能与关于解构非提升类型的previous post 有关。 关于类型提升的论文可以在here找到。

【问题讨论】：

欢迎提供标题建议。
你有不同的个实例，怎么会没有哪一个？ GHC 必须选择实例，这是一个非参数操作，因此需要一个约束。我认为你想做的事没有意义。
GHC 甚至可以通过使用显式类约束（否则会被推断）在运行时解析重叠实例（这些实例不是）。为什么它看不到有 always 匹配，即使它必须等到运行时才能选择合适的实例？当然，我要求它做到这一点没有明确的（和无偿的）类约束，我没有提供的奢侈。
@Eric，所有实例都是在编译时选择的，或者作为从约束生成的参数传入。运行时没有解决任何问题。
@Eric：因为实例做不同的事情。 非参数化中的点总是需要一个约束。临时多态性是临时的。

标签： haskell pattern-matching higher-kinded-types type-kinds

【解决方案1】：

这不是您想要的，但非常接近。我从

开始

data Proxy a where
  Proxy :: ListLen a => Proxy

然后

data Proxy a where
  Proxy :: Tagged a Int -> Proxy a

导致

test4 :: (Proxy (HList qs)) -> Int
test4 (Proxy len) = untag len

问题是您要么需要约束，要么让Proxy 包含所需类的证据（即使所有可用类型都存在实例）。这里，类方法只是包含在Proxy中。

一个完全不同的选择是根本不使用类型类，并以通常的方式实现len（转录自Data.List.length）。

len :: HList a -> Int
len l = len' l 0
  where
    len' :: HList a -> Int -> Int
    len' HNil a = a
    len' (HCons _ xs) a = len' xs $! a + 1

【讨论】：