haskell - 可以将多态常量映射到 *types* 列表上吗？

Question

Haskell 爱好者在这里 - 是否可以以通用方式将多态常量映射到类型列表上？
更准确地说，考虑这个片段:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
  
module Main where

import Data.Kind( Type )

class HasName a where name :: String

instance HasName Int where name = "Int"

instance HasName Double where name = "Double"


class AllNames (ts :: [Type]) where
  allNames :: [String]

instance AllNames '[] where
  allNames = []

instance (HasName t, AllNames rest) => AllNames (t ': rest) where
  allNames = name @t : allNames @rest

  
main :: IO ()
main = print $ allNames @'[Int, Double]

不出所料，这按预期工作，即打印 ["Int","Double"] .但是，如果我尝试概括上面的模式，以便代码可以与 一起使用任意 name -like 多态常量，然后我遇到了问题。
这是我的泛化尝试:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
  
module Main where

import Data.Kind( Constraint, Type )

--
-- Intended to be the generalized version of 'name'
--
type PolymorphicConstant (c :: Type -> Constraint) (a :: Type) = forall t . c t => a

--
-- Intended to be the generalized version of 'AllNames'
--
class AllPolymorphicConstants (c :: Type -> Constraint) (ts :: [Type]) (a :: Type) where
  allPolymorphicConstants :: PolymorphicConstant c a -> [ a ]

instance AllPolymorphicConstants c '[] a where
  allPolymorphicConstants _ = []

instance (c t, AllPolymorphicConstants c rest a) => AllPolymorphicConstants c (t ': rest) a where
  allPolymorphicConstants f = f @t : allPolymorphicConstants @c @rest @a f

唉，这不能编译(顺便说一句，我使用的是 GHC 8.10.7):

Main.hs:31:74: error:
    • Could not deduce: c t0 arising from a use of ‘f’
      from the context: (c t, AllPolymorphicConstants c rest a)
        bound by the instance declaration at Main.hs:30:10-91
      or from: c t1
        bound by a type expected by the context:
                  PolymorphicConstant c a
        at Main.hs:31:74
    • In the fourth argument of ‘allPolymorphicConstants’, namely ‘f’
      In the second argument of ‘(:)’, namely
        ‘allPolymorphicConstants @c @rest @a f’
      In the expression: f @t : allPolymorphicConstants @c @rest @a f
    • Relevant bindings include
        f :: PolymorphicConstant c a (bound at Main.hs:31:27)
        allPolymorphicConstants :: PolymorphicConstant c a -> [a]
          (bound at Main.hs:31:3)
   |
31 |   allPolymorphicConstants f = f @t : allPolymorphicConstants @c @rest @a f
   |                                                                          ^

我可能遗漏了一些基本的东西，使这种概括变得不可能——但它到底是什么？

Answer 1

我希望有人能证明我错了，但这是我们遇到当前 GHC 限制的少数极端情况之一，我们无法摆脱使用 Proxy , Tagged或类似的过去“遗物”。
一个最小的例子
让我们考虑一个更简单的例子:

class C a where

-- Ambiguous type
type T a = forall t. C t => a

请注意，如果我们有一个值 x :: T a ，除了显式类型参数 x @t 外，没有明确的使用方法。 .这是使用模棱两可的类型所要付出的代价，但这很好。
以下代码按预期进行类型检查。

foo :: forall t a. (C t) => T a -> a
foo f = f @t

相反，事实并非如此。

-- Error: Could not deduce (C t0) arising from a use of `foo'
foo2 :: forall t a. (C t) => T a -> a
foo2 = foo

起初这可能令人惊讶。确实， foo2具有完全相同的类型 foo , 所以 foo2=foo明明没问题!然而，它失败了。原因再次是模棱两可的类型，而经验法则仍然是:如果某物具有模棱两可的类型，如果我们不传递额外的 @t @a，我们就不能使用它。论据。
这样做会使一切正常。

foo3 :: forall t a. (C t) => T a -> a
foo3 = foo @t @a

上面有点奇怪，因为我们不能写(也不必写) foo3 @t @a = foo @t @a .我想如果 GHC 强制我们这样做，那么它也可以让我们“eta-contract the type arguments”一切并写 foo3 = foo .
现在，如果我们对 value 参数(而不是类型!)进行 eta-expand 怎么办。我们得到一个错误:

-- Error: Could not deduce (C t0) arising from a use of `x'
foo4 :: forall t a. (C t) => T a -> a
foo4 x = foo @t @a x

呻吟。这只是 foo3 = foo @t @a eta 扩展。这里出了什么问题？好吧，问题是一样的:现在我们介绍了 x :: T a ，这是一个模棱两可的类型，所以我们不能使用 x没有 @...论据。即使 foo期望多态值!
在这里，我们发现自己无法逃脱。 GHC 看到多态参数并在 x 上添加隐式类型参数抽象。 , 添加 (\@t0 -> ...在前。但这是我们不允许使用的一种语法，没有办法捕获新鲜的类型变量 t0 .换句话说，我们想写

foo4 :: forall t a. (C t) => T a -> a
foo4 x = foo @t @a (\@t0 -> x @t0)

但我们只能写

foo4 :: forall t a. (C t) => T a -> a
foo4 x = foo @t @a (x @something)

也没有办法提 t0那里。叹。
使用代理
我可以看到它使用的唯一“解决方案” Proxy (或类似的遗物)，并避免模棱两可的类型。

-- No longer ambiguous
type T a = forall t. C t => Proxy t -> a

foo :: forall t a. (C t) => T a -> a
foo f = f (Proxy @t)

foo4 :: forall t a. (C t) => T a -> a
foo4 x = foo @t @a x

现在我们可以使用 x原样，因为它不再具有模棱两可的类型。
使用 Tagged或将多态值包装在 newtype 中或 data也可以，因为它使类型不再模棱两可。
原始代码，代理字段

type PolymorphicConstant (c :: Type -> Constraint) (a :: Type) 
   = forall t . c t => Proxy t -> a

--
-- Intended to be the generalized version of 'AllNames'
--
class AllPolymorphicConstants (c :: Type -> Constraint) (ts :: [Type]) (a :: Type) where
  allPolymorphicConstants :: PolymorphicConstant c a -> [ a ]

instance AllPolymorphicConstants c '[] a where
  allPolymorphicConstants _ = []

instance (c t, AllPolymorphicConstants c rest a) 
    => AllPolymorphicConstants c (t ': rest) a where
  allPolymorphicConstants f = f (Proxy @t) : allPolymorphicConstants @c @rest @a f