Sí, aunque no en Haskell. Pero la orden superior cálculo lambda polimórfica (también conocido como Sistema F-omega) es más general:
bi : forall m n a b. (forall a. m a -> n a) -> m a -> m b -> (n a, n b)
bi {m} {n} {a} {b} f x y = (f {a} x, f {b} y)
x1 : (Integer, Char)
x1 = bi {\a. List a} {\a. a} {Integer} {Char} head [2,3] "45"
x2 : (Integer, Char)
x2 = bi {\a . exists b. (a, b)} {\a. a} {Integer} {Char} (\{a}. \p. unpack<b,x>=p in fst {a} {b} x) (pack<Char, (2,'3')>) (pack<Integer, ('4',5)>)
x3 : (Integer, Double)
x3 = bi {\a. a} {\a. a} {Integer} {Double} (1+) 2 3.45
Aquí, escribo f {T}
para la aplicación explícita de tipos y asumir una biblioteca mecanografiado, respectivamente. Algo como \a. a
es un lambda de tipo de nivel. El ejemplo x2
es más intrincado, porque también necesita tipos existenciales para "olvidar" localmente el otro fragmento de polimorfismo en los argumentos.
En realidad se puede simular esta en Haskell definiendo un newtype
o tipo de datos diferente para cada m
o n
se ejemplariza con, y pase funciones adecuadamente envueltos f
que agregar y quitar constructores en consecuencia. Pero, obviamente, eso no es divertido en absoluto.
Editar: Debo señalar que esto todavía no es una solución general totalmente. Por ejemplo, no puedo ver cómo se puede escribir
swap (x,y) = (y,x)
x4 = bi swap (3, "hi") (True, 3.1)
incluso en el Sistema F-omega.El problema es que la función swap
es más polimórfica que bi
y, a diferencia de x2
, la otra dimensión polimórfica no se olvida en el resultado, por lo que el truco existencial no funciona. Parece que necesitarías un polimorfismo bueno para permitirlo (de modo que el argumento bi
puede ser polimórfico en un número variable de tipos).
No lo creo. Tendría que cuantificarlo en todos los tipos de entrada, lo que requiere un resumen sobre las restricciones de clase de clase. –
@LouisWasserman, hay algunas cosas nuevas (ConstraintKinds) que permiten abstraer las restricciones. – aemxdp
Bien, veo eso, pero no creo que puedas cuantificar los tipos de resultados como lo harías. Si tuviera la forma 'a -> a', podría hacer' bi :: (cxt a, cxt b) => (forall x. Cxt x => x -> x) -> a -> b -> (a, b) ', pero no creo que pueda obtener automáticamente la" función de tipo "de cada entrada para su tipo de resultado. –