haskell - son - sinonimos wikipedia

¿Por qué TypeSynonymInstances no permite que se utilicen sinónimos de tipo aplicados parcialmente en los cabezales de instancia?

Question

Sé que TypeSynomymInstances solo permite que se usen sinónimos de tipo completamente aplicados en los encabezados de instancia , pero parece que sería útil si pudiera usar sinónimos de tipo aplicados paritalmente para usarlos también.

Por ejemplo:

class Example e where
thingy :: a -> b -> e a b
-- legit, but awkward
newtype FuncWrapper e a b = FuncWrapper { ap :: a -> e a b }
instance (Example e) => Example (FuncWrapper e) where
thingy _ = FuncWrapper . flip thingy
funcWrapperUse :: (Example e) => e Int String
funcWrapperUse = thingy 1 "two" `ap` 3 `ap` 4 `ap` 5
-- not legal, but a little easier to use
type FuncSynonym e a b = a -> e a b
instance (Example e) => Example (FuncSynonym e) where
thingy _ = flip thingy
funcSynonymUse :: (Example e) => e Int String
funcSynonymUse = thingy 1 "two" 3 4 5

Answer 1

Los sinónimos de tipo aplicados parcialmente no están permitidos en absoluto en Haskell. Un sinónimo parcialmente aplicado es efectivamente una función cuyas entradas son los tipos no aplicados y cuyo resultado es un tipo. Por ejemplo, aquí hay una codificación de lógica booleana:

type True x y = x
type False x y = y
type Not b x y = b y x
type And b1 b2 x y = b1 (b2 x y) y
type Or b1 b2 x y = b1 x (b2 x y)

Para decidir si dos sinónimos de tipo parcialmente aplicados son iguales, el verificador de tipos debería decidir si las funciones son iguales. Este es un problema difícil, y en general es indecidible.

Answer 2

Otro problema con permitir sinónimos de tipo aplicados parcialmente es que harían la inferencia de tipos y la selección de instancias esencialmente imposibles. Por ejemplo, supongamos que, en el contexto de algún programa, quería usar thingy en el tipo Int -> String -> Int -> (Int, String) . thingy tiene type forall ab e. a -> b -> eab forall ab e. a -> b -> eab , entonces podemos unificar a con Int b con String , pero si se permite que e sea un sinónimo de tipo parcialmente aplicado, podríamos tener

e = FuncSynonym (,)

o

e = FuncSynonym'' Int (,) where type FuncSynonym'' x f a b = x -> f a b

o incluso

e = Const2 (Int -> (Int, String)) where Const2 a x y = a

El problema de la inferencia de tipo sería incluso peor que decidir la igualdad de funciones; requeriría considerar todas las funciones con salida especificada en una entrada particular, o problemas más complicados similares (imagínese simplemente tratando de unificar ab con Int ).