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

Question

在讨论VoidHaskell Libraries 邮件列表时，有这样的评论：

回到过去，它曾经是由unsafeCoerceConor McBride 的要求实现的，他不想为遍历整个Functor 内容和替换其内容而付费，而类型告诉我们它不应该有任何内容。如果应用于适当的 Functor，这是正确的，但在 GADT 存在的情况下是可颠覆的。

的文档unsafeVacuous还说：

IfVoid是无人居住的，比任何Functor只持有该类型值的人Void都不持有任何值。

这仅对不对参数执行类似 GADT 分析的有效函子是安全的。

这样一个恶作剧的 GADTFunctor实例会是什么样子？（当然只使用总函数，不使用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
  ...

whereSomething是任何不是普通变量的类型，那么我们不能Functor为F. 为了遵守函子的恒等律，该fmap函数必须映射C到。C但我们必须生产一个F b，用于未知b。如果Something不是一个普通的变量，那是不可能的。