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類似的多型常量一起使用，那么我就會遇到問題。

這是我的泛化嘗試：

{-# 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
   |                                                                          ^

我可能遺漏了一些基本的東西，使這種概括變得不可能——但它到底是什么？

uj5u.com熱心網友回復：

我希望有人能證明我錯了，但這是我們遇到當前 GHC 限制的少數極端案例之一，我們無法擺脫使用Proxy，Tagged或類似的過去“遺物”。

一個最小的例子

讓我們考慮一個更簡單的例子：

class C a where

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

請注意，如果我們有一個 value 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顯然是OK的！然而，它失敗了。原因再次是模棱兩可的型別，而經驗法則仍然是：如果某物具有模棱兩可的型別，如果我們不傳遞額外的@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

Groan. This is simply foo3 = foo @t @a eta-expanded. What's going wrong here? Well, the issue is the same: now we introduced x :: T a, and that's an ambiguous type, so we can not use x without @... arguments. Even if foo expects a polymorphic value!

Here we find ourselves unable to escape. GHC sees the polymorphic arguments and adds an implicit type argument abstraction over x, adding (\@t0 -> ... in front. But that's a kind of syntax we are not allowed to use, and there is no way to capture the fresh type variable t0. In other words, we would like to write

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

but we can only write

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

and there is no way to mention t0 there. Sigh.

Using proxies

The only "solution" I can see it to use Proxy (or similar relics), and avoid ambiguous types.

-- 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

Now we can use x as-is since it has no longer an ambiguous type.

Using Tagged or wrapping the polymorphic value inside a newtype or data would also work, since it makes the type no longer ambiguous.

The original code, proxy-fied

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

標籤：哈斯克尔 类型类

上一篇：Lenses、Statemonad和具有已知鍵的Maps

下一篇：如何檢查串列中的下一個元素是否大于Haskell中的前一個？