是否可以为涉及类型族的此数据类型编写fmap？

Question

鉴于以下类型族(应该反映同构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)

是否有可能通过某种类型的hackery Functor为后者编写实例？

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

直觉上,根据类型显而易见,该怎么做f,但我不知道如何在Haskell中表达它.

Answer 1

我倾向于推理使用Agda这类更高级的程序.

这里的问题是你想要模式匹配*(Set在Agda中),违反参数,如评论中所提到的.这不好,所以你不能这样做.你必须提供证人.即遵循是不可能的

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中对此进行编码.

您可以使用例如'惯用'Haskell类型不等式来表达它

我将把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

这些也更容易直接编码.