多态常量可以映射到*类型*列表上吗？

Question

Haskell 爱好者 - 是否可以以通用方式将多态常量映射到类型列表上？

\n

更准确地说，考虑这个片段：

\n

{-# LANGUAGE AllowAmbiguousTypes #-}\n{-# LANGUAGE DataKinds #-}\n{-# LANGUAGE KindSignatures #-}\n{-# LANGUAGE ScopedTypeVariables #-}\n{-# LANGUAGE TypeApplications #-}\n{-# LANGUAGE TypeOperators #-}\n  \nmodule Main where\n\nimport Data.Kind( Type )\n\nclass HasName a where name :: String\n\ninstance HasName Int where name = "Int"\n\ninstance HasName Double where name = "Double"\n\n\nclass AllNames (ts :: [Type]) where\n  allNames :: [String]\n\ninstance AllNames '[] where\n  allNames = []\n\ninstance (HasName t, AllNames rest) => AllNames (t ': rest) where\n  allNames = name @t : allNames @rest\n\n  \nmain :: IO ()\nmain = print $ allNames @'[Int, Double]\n

\n

不出所料，这按预期工作，即打印["Int","Double"]。但是，如果我尝试概括上面的模式，以便代码可以与任何 name类似的多态常量一起使用，那么我就会遇到问题。

\n

这是我的概括尝试：

\n

{-# LANGUAGE AllowAmbiguousTypes #-}\n{-# LANGUAGE ConstraintKinds #-}\n{-# LANGUAGE DataKinds #-}\n{-# LANGUAGE FlexibleInstances #-}\n{-# LANGUAGE KindSignatures #-}\n{-# LANGUAGE MultiParamTypeClasses #-}\n{-# LANGUAGE RankNTypes #-}\n{-# LANGUAGE ScopedTypeVariables #-}\n{-# LANGUAGE TypeApplications #-}\n{-# LANGUAGE TypeOperators #-}\n  \nmodule Main where\n\nimport Data.Kind( Constraint, Type )\n\n--\n-- Intended to be the generalized version of 'name'\n--\ntype PolymorphicConstant (c :: Type -> Constraint) (a :: Type) = forall t . c t => a\n\n--\n-- Intended to be the generalized version of 'AllNames'\n--\nclass AllPolymorphicConstants (c :: Type -> Constraint) (ts :: [Type]) (a :: Type) where\n  allPolymorphicConstants :: PolymorphicConstant c a -> [ a ]\n\ninstance AllPolymorphicConstants c '[] a where\n  allPolymorphicConstants _ = []\n\ninstance (c t, AllPolymorphicConstants c rest a) => AllPolymorphicConstants c (t ': rest) a where\n  allPolymorphicConstants f = f @t : allPolymorphicConstants @c @rest @a f\n\n

\n

唉，这无法编译（顺便说一句，我正在使用 GHC 8.10.7）：

\n

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

\n

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

\n

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 收缩类型参数”一切并编写foo3 = foo.

现在，如果我们 eta 扩展值参数（而不是类型！）。我们得到一个错误：

-- 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 @aeta 扩展。这里出了什么问题？好吧，问题是一样的：现在我们引入了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原样使用，因为它不再是模糊的类型。

在or中使用Tagged或包装多态值也可以，因为它使类型不再模糊。newtypedata

原始代码，代理化

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