haskell - 如何创建一个正确的多态 Functor 实例在 unsafeVacuous 上失败？

Question

讨论时Void在 Haskell 库邮件列表中，有 this remark :

Back in the day it used to be implemented by an unsafeCoerce at the behest of Conor McBride who didn't want to pay for traversing the whole Functor and replacing its contents, when the types tell us that it shouldn't have any. This is correct if applied to a proper Functor, but subvertible in the presence of GADTs.

unsafeVacuous 的文档还说:

If Void is uninhabited than any Functor that holds only values of the type Void is holding no values.

This is only safe for valid functors that do not perform GADT-like analysis on the argument.

这么调皮的GADT怎么会Functor实例是什么样的？ (当然只使用全部函数，不使用 undefined 、 error 等)

Answer 1

如果您愿意提供 Functor，这当然是可能的。不遵守仿函数定律的实例(但全部):

{-# LANGUAGE GADTs, KindSignatures #-}

import Data.Void
import Data.Void.Unsafe

data F :: * -> * where
  C :: F Void
  D :: F a

instance Functor F where
  fmap f _ = D

wrong :: ()
wrong = case (unsafeVacuous C :: F Int) of D -> ()

正在评估wrong导致运行时异常，即使类型检查器认为它全部。

编辑

因为关于仿函数性的讨论太多了，让我补充一个非正式的论点，为什么实际对其参数进行分析的 GADT 不能是仿函数。如果我们有

data F :: * -> * where
  C :: ... -> F Something
  ...

哪里Something是任何不是普通变量的类型，那么我们不能给出有效的 Functor F 的实例. fmap函数必须映射 C至 C为了遵守仿函数的恒等律。但是我们必须产生一个 F b , 对于未知 b .如 Something只是一个普通的变量，这是不可能的。