¿Haskell, o un comstackdor específico, tiene algo así como lambdas de nivel de tipo (si es incluso un término)?
Para dar más detalles, digamos que tengo un tipo parametrizado Foo ab
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 ab) where ...
?
De TypeCompose:
newtype Flip (~>) ba = 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, puede hacerlo un bifunctor:
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 )
Mientras sclv responde su pregunta directa, añadiré aparte que hay más de un significado posible para “lambda de nivel de tipo”. Haskell tiene una variedad de operadores tipo, pero ninguno realmente se comporta como lambdas propiamente dicho:
A
y un constructor de tipo F
, la aplicación de función FA
también es un tipo, pero no lleva más información (nivel de tipo) que “esto es F
aplicado a A
“. a -> b -> a
implícitamente significa por forall a b. a -> b -> a
forall a b. a -> b -> a
. forall
vincula las variables de tipo dentro de su scope, comportándose así algo así como una lambda. Si la memoria me sirve, esta es más o menos la “capital lambda” en el Sistema F. 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 scope vinculante con una abstracción de función anónima.
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.
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 de tipo dependiente. Te recomiendo que uses un lenguaje dependiente, como Agda (similar a Haskell) o Coq (diferente, pero todavía funcional puro en su núcleo, y puede ser interpretado y comstackdo de forma perezosa o estricta). Pero estoy predispuesto hacia esos idiomas ¡y esto es probablemente 100 veces más de lo que está pidiendo aquí!
Lo más cerca que sé de obtener un tipo lambda es definir un tipo sinónimo. En tu ejemplo,
data Foo ab = Foo ab type FooR ab = Foo ba 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.
Sí, lo que dijo Gabe, que es un tanto respondido por las familias de tipos: