Можно ли написать fmap для этого типа данных, включающего семейство типов?

Учитывая следующее семейство типов (предполагается, что оно отражает изоморфизм 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
person Sebastien    schedule 14.01.2015    source источник
comment
Мое чутье говорит, что это невозможно, так как это должно нарушить параметричность.   -  person Cactus    schedule 14.01.2015

Ответы (1)


arrow_upward
12
arrow_downward

Я склонен рассуждать об этих добрых более высоких программах, использующих 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

Их также проще закодировать напрямую.

person phadej    schedule 14.01.2015