相关疑难解决方法(0)

因此,在我不断尝试通过小型Haskell练习半理解Curry-Howard时,我已经陷入了困境:

{-# LANGUAGE GADTs #-}

import Data.Void

type Not a = a -> Void

-- | The type of type equality proofs, which can only be instantiated if a = b.
data Equal a b where
    Refl :: Equal a a

-- | Derive a contradiction from a putative proof of @Equal Int Char@.
intIsNotChar :: Not (Equal Int Char)
intIsNotChar intIsChar = ???

很明显,这种类型Equal Int Char没有(非底层)居民,因此在语义上应该有一个absurdEquality :: Equal Int Char -> a功能......但对于我的生活,我无法想出任何方式来编写除了使用之外的其他方法undefined.

所以要么: …

鉴于以下类型族(应该反映同构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中表达它.