tipos simbolos opciones multiplicar hacer funciones ejemplos como basico haskell lambda

simbolos - string en haskell



Lambda para expresiones de tipo en Haskell? (6)

¿Haskell, o un compilador 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 a b) where ...

?

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

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 compilado 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 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.

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:

  • Constructores de 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 FA también es un tipo, pero no lleva más información (nivel de tipo) que "esto es F aplicado a A ".
  • Tipos polimórficos: un tipo como 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 alcance, 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.
  • Escriba sinónimos: una forma limitada de operadores de tipo que se debe aplicar por completo, y solo puede producir tipos de base y constructores de tipo.
  • Clases de tipos : Esencialmente funciones de tipos / tipos constructores a valores, con la capacidad de inspeccionar el argumento tipo (es decir, por coincidencia de patrones en constructores de tipos aproximadamente del mismo modo que el patrón de funciones regulares coincide con los constructores de datos) y que sirve para definir una membresía predicado sobre tipos. Estos se comportan más como una función normal en algunos aspectos, pero son muy limitados: las clases de tipos no son entidades de primera clase que pueden manipularse, y operan en tipos solo como entrada (no salida) y valores solo como salida ( definitivamente no entrada).
  • Dependencias funcionales: junto con algunas otras extensiones, éstas 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, por ejemplo, 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.

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.