是否可以为这种涉及类型族的数据类型编写 fmap？答案

【问题标题】：Is it possible to write fmap for this data type involving a type family?是否可以为这种涉及类型族的数据类型编写 fmap？
【发布时间】：2015-01-14 16:15:08
【问题描述】：

给定以下类型族（应该反映同构 A×1 ≅ A）

type family P (x :: *) (a :: *) :: * where
  P x () = x
  P x a  = (x, a)

及其定义的数据类型

data T a = T Integer (P (T a) a)

某种类型的黑客是否有可能为后者编写Functor 实例？

instance Functor T where
  fmap f = undefined  -- ??

直观地说，根据f的类型，很明显该做什么，但我不知道如何用Haskell表达。

【问题讨论】：

我的直觉认为这是不可能的，因为它需要违反参数化。

标签： haskell ghc type-families

【解决方案1】：

我倾向于使用 Agda 来推理这些高级程序。

这里的问题是你想在*（Agda 中的Set）上进行模式匹配，违反了注释中提到的参数性。这不好，所以你不能就这样去做。你必须提供证人。 IE。以下是不可能的

P : Set → Set → Set
P Unit b = b
P a b = a × b

您可以通过使用辅助类型来克服限制：

P : Aux → Set → Set
P auxunit b     = b
P (auxpair a) b = a × b

或者在 Haskell 中：

data Aux x a = AuxUnit x | AuxPair x a

type family P (x :: Aux * *) :: * where
  P (AuxUnit x) = x
  P (AuxPair x a) = (x, a)

但是这样做你会遇到表达T 的问题，因为你需要再次对其参数进行模式匹配，以选择正确的Aux 构造函数。

“简单”的解决方案，是在a ~ ()时表达T a ~ Integer，直接T a ~ (Integer, a)：

module fmap where

record Unit : Set where
  constructor tt

data ⊥ : Set where

data Nat : Set where
  zero : Nat
  suc : Nat → Nat

data _≡_ {ℓ} {a : Set ℓ} : a → a → Set ℓ where
  refl : {x : a} → x ≡ x

¬_ : ∀ {ℓ} → Set ℓ → Set ℓ
¬ x = x → ⊥

-- GADTs
data T : Set → Set1 where
  tunit : Nat → T Unit
  tpair : (a : Set) → ¬ (a ≡ Unit) → a → T a

test : T Unit → Nat
test (tunit x) = x
test (tpair .Unit contra _) with contra refl
test (tpair .Unit contra x) | ()

您可以尝试在 Haskell 中将其编码为。

您可以使用例如'idiomatic' Haskell type inequality

我将 Haskell 版本作为练习 :)

嗯还是你说的data T a = T Integer (P (T a) a)：

T () ~ Integer × (P (T ()) ())
     ~ Integer × (T ())
     ~ Integer × Integer × ... -- infinite list of integers?

-- a /= ()
T a ~ Integer × (P (T a) a)
    ~ Integer × (T a × a) ~ Integer × T a × a
    ~ Integer × Integer × ... × a × a

那些也更容易直接编码。

【讨论】：