Lambda para expresiones de tipo en Haskell?

Question

¿Haskell, o un compilador específico, tiene algo así como lambdas de nivel de tipo (si es incluso un término)?

Para elaborar, decir que tengo un tipo parametrizado Foo a b y quiero que Foo _ b sea una instancia de, digamos, Functor. ¿Hay algún mecanismo que me permita hacer algo similar a

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

?

Answer 1

De 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

Además, si algo es un Functor en dos argumentos, que puede hacer que sea un bifuntor:

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

(o, en una categoría posterior-extras, una versión más general: http://hackage.haskell.org/packages/archive/category-extras/0.53.5/doc/html/Control-Functor.html#t:Bifunctor)

Answer 2

Lo más cercano que conozco para obtener un tipo lambda es definir un tipo sinónimo. En su ejemplo,

data Foo a b = Foo a b 

type FooR a b = Foo b a 

instance Functor (FooR Int) where 
... 

Pero incluso con -XTypeSynonymInstances -XFlexibleInstances esto no funciona; GHC espera que el tipo syn se aplique por completo en el encabezado de la instancia. Puede haber alguna manera de organizarlo con familias de tipos.

Answer 3

No me gusta la idea de responder mi propia pregunta, pero aparentemente, según varias personas en #haskell en Freenode, Haskell no tiene lambdas de nivel de tipo.

Answer 4

Sí, lo dijo Gabe, que es algo contestada por las familias de tipo:

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

Answer 5

Mientras SCLV respondido a su pregunta directa, voy a añadir como un aparte de que hay más de un significado posible para "Tipo "nivel lambda". Haskell tiene una variedad de operadores de tipo, pero ninguno realmente se comportan como lambdas adecuados:

• constructores Tipo: operadores de tipo abstracto que introducen nuevos tipos. Dado un tipo A y un constructor de tipo F, la aplicación de función F A también es un tipo pero no lleva información adicional (nivel de tipo) que "esto es F aplicado a A".
• Tipos polimórficos: Un tipo como a -> b -> a implícitamente significa forall a b. a -> b -> a. El forall vincula las variables de tipo dentro de su alcance, comportándose así algo así como un lambda. Si la memoria me sirve, esta es más o menos la "capital lambda" en el Sistema F.
• Escriba sinónimos: Una forma limitada de operadores de tipo que se debe aplicar completamente, y solo puede producir tipos base y constructores de tipo.
• Clases de tipos: Funciona esencialmente desde tipos/tipos de constructores hasta valores, con la capacidad de inspeccionar el argumento de tipo (es decir, por coincidencia de patrones en constructores de tipos aproximadamente de la misma manera que el patrón de funciones regulares coincide con los constructores de datos) y que sirve para definir un predicado de pertenencia sobre tipos. Estos se comportan más como una función normal de alguna manera, pero son muy limitados: las clases de tipo no son entidades de primera clase que pueden manipularse, y operan en tipos solo como entrada (no salida) y valores solo como salida (definitivamente sin entrada).
• Dependencias funcionales: Junto con algunas otras extensiones, estas permiten que las clases de tipos generen implícitamente también tipos como resultados, que luego pueden usarse como parámetros para otras clases de tipos. Todavía muy limitado, p. al no poder tomar otras clases de tipos como argumentos.
• Familias tipo: Un enfoque alternativo a lo que hacen las dependencias funcionales; permiten que las funciones en los tipos se definan de una manera que se ve mucho más cerca de las funciones de nivel de valor regulares. Las restricciones habituales todavía se aplican, sin embargo.

Otras extensiones relajan algunas de las restricciones mencionadas, o proporcionan soluciones parciales (ver también: hackers tipo Oleg). Sin embargo, más o menos lo único que no puedes hacer en ningún lado es exactamente lo que preguntaste, es decir, introducir un nuevo alcance vinculante con una abstracción de función anónima.

Answer 6

EHC (y quizás también su sucesor, UHC) tiene lambdas de nivel de tipo, pero no están documentadas y no son tan potentes como en un lenguaje dependiente. Te recomiendo que uses un lenguaje de tipo dependiente como Agda (similar a Haskell) o Coq (diferente, pero todavía funcional puro en su núcleo, y puede interpretarse y compilarse o bien perezosamente o estrictamente). Pero estoy predispuesto a ¡Tales idiomas, y esto es probablemente 100 veces más de lo que está pidiendo aquí!