유형 패밀리가 관련된이 데이터 유형에 대해 fmap을 작성할 수 있습니까?

Question

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

이들의 관점에서 정의

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

데이터 입력합니다 (동형 × 1 ≅ 반영 가정) 다음과 같은 종류의 계열이 주어은 가능한 일부 타입의 해커에 의해 작성하는 후자에 대한 인스턴스 Functor?

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

직관적으로, 그것은 f의 종류에 따라 할 것을 분명하지만, 나는 하스켈에서 그것을 표현하는 방법을 모르겠어요.

Answer 1

나는 Agda를 사용하는 이러한 종류의 더 높은 종류의 프로그램에 대해 추론하는 경향이 있습니다.

여기서 문제는 덧글에서 언급 한 것처럼 * (Agda의 Set)에서 패턴 매치를하고 매개 변수를 위반한다는 것입니다. 그건 좋지 않아서, 당신은 그것을 할 수 없습니다. 증인을 제공해야합니다. 나는. ,

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을 표현해야하고 :

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

또는 하스켈 : 다음은 보조 형식을 사용하여 limitiation을 극복 할 수

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

수 없습니다 매개 변수에 패턴 일치를 다시해야하므로 오른쪽 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) |() 

당신은 하스켈에이 인코딩 시도 할 수 있습니다.

예 : 'idiomatic' Haskell type inequality

나는 :) 연습으로

---

흠을 하스켈 버전을 떠날거야하거나 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 

사람들은 직접뿐만 아니라 인코딩하기가 더 쉽습니다.