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

Question

给定以下类型族(应该反射(reflect)同构 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 来表达。

Answer 1

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

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

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

您可以通过使用 aux 类型来克服限制:

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构造函数。

“简单”的解决方案，就是表达 T a ~ Integer当 a ~ () , 和 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

这些也更容易直接编码。