È possibile scrivere fmap per questo tipo di dati che coinvolgono una famiglia di tipi?

Question

Data la famiglia seguente tipo (dovrebbe riflettere l'isomorfismo A × 1 ≅ A) Tipo

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

e dati definito in termini della stessa

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

è possibile da qualche tipo aggiustamenti per scrivere Functor istanza per quest'ultimo?

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

Intuitivamente, è ovvio cosa fare a seconda del tipo di f, ma non so come esprimerlo in Haskell.

Answer 1

Tendo a ragionare su questi programmi di tipo più gentile utilizzando Agda.

Il problema qui è che si desidera modello match * (Set in Agda), violi parametericity, come accennato nel commento. Non va bene, quindi non puoi farlo. Devi fornire un testimone. Cioè segue non è possibile

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

È possibile superare la limitiation utilizzando aux Tipo:

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

O in 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) 

Ma così facendo avrai problemi esprimere T, poiché è necessario ripetere la corrispondenza dei parametri sui propri parametri, per selezionare il costruttore di destra Aux.

---

soluzione "semplice", è quello di esprimere T a ~ Integer quando a ~(), e T a ~ (Integer, a) direttamente:

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) |() 

Si può cercare di codificare questo in Haskell a.

È possibile esprimerlo utilizzando, ad es. 'idiomatic' Haskell type inequality

Lascio la versione Haskell come esercizio :)

---

Hmm o hai intendevo per 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 

Quelli sono più facili da codificare direttamente pure.