Lambda per le espressioni di tipo in Haskell?

Question

Haskell, o un compilatore specifico, ha qualcosa come lambda di tipo di livello (se è addirittura un termine)?

Per elaborare, dire che ho un tipo parametrizzato Foo a b e voglio che Foo _ b sia un'istanza di, diciamo, Functor. C'è qualche meccanismo che mi permetterebbe di fare qualcosa di simile a

instance Functor (\a -> Foo a b) where 
... 

?

Answer 1

Da TypeCompose:

newtype Flip (~>) b a = Flip { unFlip :: a ~> b } 

http://hackage.haskell.org/packages/archive/TypeCompose/0.6.3/doc/html/Control-Compose.html#t:Flip

Inoltre, se qualcosa è un funtore a due argomenti, si può fare un bifunctor:

http://hackage.haskell.org/packages/archive/category-extras/0.44.4/doc/html/Control-Bifunctor.html

(o, in una versione successiva, una versione più generale: http://hackage.haskell.org/packages/archive/category-extras/0.53.5/doc/html/Control-Functor.html#t:Bifunctor)

Answer 2

Il più vicino che conosco per ottenere un tipo lambda consiste nel definire un sinonimo di tipo. Nel tuo esempio,

data Foo a b = Foo a b 

type FooR a b = Foo b a 

instance Functor (FooR Int) where 
... 

Ma anche con -XTypeSynonymInstances -XFlexibleInstance questo non funziona; GHC si aspetta che il tipo syn sia completamente applicato nella testata dell'istanza. Potrebbe esserci un modo per organizzarlo con famiglie di tipi.

Answer 3

Non mi piace l'idea di rispondere alla mia domanda, ma a quanto pare, secondo diverse persone su #haskell su Freenode, Haskell non ha lambda di livello tipo.

Answer 4

Sì, quello che ha detto Gabe, che è in qualche modo risposto dalle famiglie tipo:

http://www.haskell.org/haskellwiki/GHC/Type_families

Answer 5

Mentre SCLV risposto alla tua domanda diretta, aggiungerò come divagazione che c'è più di un significato possibile per "tipo di -level lambda ". Haskell ha una varietà di operatori di tipo ma nessuno in realtà si comportano come lambda corrette:

• Tipo costruttori: astratte di tipo operatori che introducono nuovi tipi. Dato un tipo A e un costruttore di tipi F, l'applicazione di funzione F A è anche un tipo ma non riporta ulteriori informazioni (di tipo livello) di "questo è F applicato a A".
• Tipi polimorfici: Un tipo come a -> b -> a significa implicitamente forall a b. a -> b -> a. Lo forall associa le variabili di tipo all'interno del suo ambito, comportandosi in qualche modo come un lambda. Se la memoria mi serve è approssimativamente la "capitale lambda" nel Sistema F.
• Tipo di sinonimi: Una forma limitata di operatori di tipi che devono essere completamente applicati e in grado di produrre solo tipi di base e costruttori di tipi.
• Classi di tipo: Principalmente funzioni da tipi/tipi di costruttori a valori, con la possibilità di ispezionare l'argomento del tipo (ad es., mediante la corrispondenza dei modelli sui costruttori di tipi in modo approssimativo nello stesso modo in cui il modello di funzioni regolari corrisponde ai costruttori di dati) e serve a definire un predicato di appartenenza sui tipi. Questi comportamenti si comportano in qualche modo come una funzione normale, ma sono molto limitati: le classi di tipi non sono entità di prima classe che possono essere manipolate e operano sui tipi solo come input (non di output) e valori solo come output ( non inserito).
• Dipendenze funzionali: Insieme ad altre estensioni, queste consentono alle classi di tipi di produrre implicitamente anche i tipi come risultati, che possono quindi essere utilizzati come parametri per altre classi di tipi. Ancora molto limitato, ad es. non essendo in grado di prendere altre classi di tipi come argomenti.
• Famiglie di tipi: Un approccio alternativo a ciò che fanno le dipendenze funzionali; consentono alle funzioni sui tipi di essere definite in un modo che sembra molto più vicino alle normali funzioni a livello di valore. Le normali restrizioni si applicano comunque.

Altre estensioni rilassa alcune delle restrizioni menzionate o forniscono soluzioni alternative (vedere anche: tipo di hacker di Oleg). Tuttavia, praticamente l'unica cosa che non puoi fare in alcun modo è esattamente quello che stavi chiedendo, ovvero introdurre un nuovo ambito di legame con un'astrazione di funzione anonima.

Answer 6

EHC (e forse anche il suo successore, UHC) ha lambda di livello testo, ma non sono documentati e non sono potenti come in un linguaggio tipizzato in modo dipendente. Vi consiglio di usare un linguaggio tipizzato come Agda (simile a Haskell) o Coq (diverso, ma puramente funzionale al suo interno, e può essere interpretato e compilato pigramente o rigorosamente!) Ma sono prevenuto verso tali lingue, e questo è probabilmente 100x overkill per quello che stai chiedendo qui!