Compilatori di tipi come funzioni

Question

Recentemente mi sono imbattuto in una situazione in cui volevo essere in grado di comporre costruttori di tipi in una dichiarazione di istanza. Mi sarebbe piaciuto fare questo:

instance (SomeClass t, SomeClass t') => SomeClass (t . t') where 

con (t . t') definito tale che (t . t') a = t (t' a) (così t e t' hanno tipo * -> * Possiamo parzialmente applichiamo costruttori di tipo, come le funzioni, quindi qual è il motivo per cui non possiamo comporre.? inoltre, c'è forse una soluzione per quello che stavo cercando di realizzare forse con vincoli di uguaglianza

(so che Control.Compose esiste, ma crea semplicemente un wrapper newtype - Vorrei un tipo sinonimo)??.

Answer 1

(so che esiste Control.Compose, ma crea semplicemente un wrapper newtype - Vorrei un sinonimo di tipo).

Questo non è consentito in Haskell. Un sinonimo di tipo deve essere applicato completamente: non è possibile scrivere , solo Compose t t' a.

Permettere sinonimi tipo richiesti parzialmente porterebbe a lambda tipo di livello, che rende inferenza di tipo indecidibile, quindi la mancanza di supporto per esso in Haskell.

---

Ad esempio, (consentire tutte le estensioni GHC rilevanti)

type Compose t t' a = t (t' a) 
data Proxy (k :: * -> *) = Proxy 

pr :: Proxy (Compose [] []) 
pr = Proxy 

risultati in:

Type synonym ‘Compose’ should have 3 arguments, but has been given 2 
    In the type signature for ‘pr’: pr :: Proxy (Compose [] []) 

Analogamente,

class C k where f :: k Int -> Int 
instance C (Compose [] []) where f _ = 6 

rendimenti:

Type synonym ‘Compose’ should have 3 arguments, but has been given 2 
    In the instance declaration for ‘C (Compose [] [])’ 

Ecco un esempio dove tipo sinonimi applicazione parziale è permesso, invece (abilitazione LiberalTypeSynonyms):

type T k = k Int 
type S = T (Compose [] []) 

bar :: S -> S 
bar = map (map succ) 

nota tuttavia che questo funziona solo perché dopo espansione tradurre otteniamo un tipo completamente applicata [] ([] Int) (cioè, [[Int]]). Approssimativamente, questa funzione non consente di fare nulla che si possa fare senza di essa, espandendo manualmente i sinonimi.