没有值的 GHC TypeLits

Question

试图设计一个类型驱动的 API，我一直在尝试让类似下面的东西工作（使用更复杂的 code/attempts，这被精简到最低要求阐明我在寻找什么):

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}

module Main where

import Data.Proxy
import GHC.TypeLits

type Printer (s :: Symbol) = IO ()

concrete :: Printer "foo"
concrete = generic

generic :: KnownSymbol s => Printer s
generic = putStrLn (symbolVal (Proxy :: Proxy s))

main :: IO ()
main = concrete

这个程序会打印 'foo'，但不会：

Could not deduce (KnownSymbol s0)
  arising from the ambiguity check for ‘generic’
from the context (KnownSymbol s)
  bound by the type signature for
             generic :: KnownSymbol s => Printer s
  at test5.hs:14:12-37
The type variable ‘s0’ is ambiguous
In the ambiguity check for:
  forall (s :: Symbol). KnownSymbol s => Printer s
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature for ‘generic’:
  generic :: KnownSymbol s => Printer s

启用AllowAmbiguousTypes 并没有多大帮助。有什么方法可以让它正常工作吗？

Answer 1

这是错误的：

generic :: KnownSymbol s => Printer s
generic = ...(Proxy :: Proxy s)

最后的s和上面的s没有关系。它是局部隐式普遍量化的，就像在顶级类型注释中一样。代码实际意思是

generic :: KnownSymbol s => Printer s
generic = ...(Proxy :: forall z. Proxy z)

要解决上述问题，请启用 ScopedTypeVariables 并使用

-- the explicit forall makes s available below
generic :: forall s. KnownSymbol s => Printer s
generic = ...(Proxy :: Proxy s)

不过，正如 Tikhon Jelvis 在他的回答中指出的那样，还有其他问题。

Answer 2

类型同义词（用 type 定义）在类型检查期间被替换为它们的定义。问题是 Printer 在其定义中没有引用 s，这导致以下约束：

generic :: KnonwSymbol s => IO ()

此类型签名没有 => 的 s 权限，因此未通过歧义检查。它不能真正工作，因为没有地方可以指定 s 在你使用它时应该是什么。

不幸的是，GHC 在错误消息中表示类型同义词的方式不一致。有时它们被扩展，有时它们被保留。具有讽刺意味的是，我认为错误消息的改进使得这个特定错误更难追踪：通常，根据您定义的类型来表达错误更清楚，但在这里它隐藏了歧义的原因。

您需要的是某种方式来提供不依赖于类型同义词的相关类型级符号。但首先，您需要启用 ScopedTypeVariables 并在 generic 的签名中添加一个 forall 以确保类型签名中的 s 和类型签名中的 s Proxy :: Proxy s 相同。

有两种可能：

把Printer改成newtype用的时候解包:

newtype Printer (s :: Symbol) = Printer { runPrinter :: IO () }

generic :: forall s. KnownSymbol s => Printer s
generic = Printer $ putStrLn (symbolVal (Proxy :: Proxy s))

main = runPrinter generic

将额外的 Proxy 参数传递给 generic，就像 symbolVal:
```
concrete :: Printer "foo"
concrete = generic (Proxy :: Proxy "foo")

generic :: forall proxy s. KnownSymbol s => proxy s -> IO ()
generic _ = putStrLn (symbolVal (Proxy :: Proxy s))
```
将 proxy 作为类型变量是一个简洁的习惯用法，它让您不依赖于 Data.Proxy 并且让调用者可以代替它传递他们想要的任何内容。

没有值的 GHC TypeLits

GHC TypeLits without values

haskell

ghc