GHC TypeLits没有值

Question

试图设计一个类型驱动的API,我一直试图得到类似下面的工作(使用更复杂的代码/尝试,这被剥离到澄清我正在寻找的最低要求):

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

在类型检查期间,类型同义词(定义为type)将替换为其定义.问题是在其定义中Printer没有引用s,这导致以下约束:

generic :: KnonwSymbol s => IO ()

此类型签名没有s权限,=>因此无法进行歧义检查.它无法真正起作用,因为无法指定s使用它时应该是什么.

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

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

有两种可能性:

• 更改Printer为a 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,并让呼叫者通过在任何他们想要代替它.