¿Estoy pensando y usando tipos de singleton en Haskell correctamente?

Question

Quiero crear varios tipos de datos incompatibles, pero por lo demás iguales. Es decir, me gustaría tener un tipo parametrizado Foo a, y funciones tales como

bar :: (Foo a) -> (Foo a) -> (Foo a) 

sin encargada del cuidado acerca de lo que es a. Para aclarar aún más, me gustaría que el sistema de tipos para que dejara de hacer

x :: Foo Int 
y :: Foo Char 
bar x y 

mientras que al mismo tiempo no me importa acerca Int y Char (que sólo se preocupan de que no son lo mismo) .

En mi código actual tengo un tipo para polinomios sobre un anillo dado. En realidad, no me importa lo indeterminado, siempre que el sistema de tipo me impida agregar un polinomio en t con un polinomio en s. Hasta ahora he resuelto mediante la creación de una clase de tipos Indeterminate, y parametrización mi tipo polinomio como

data (Ring a, Indeterminate b) => Polynomial a b 

Este enfoque se siente perfectamente natural para la parte Ring porque yo hago cuidado sobre dicho anillo particular un polinomio dado ha terminado . Se siente muy artificial para la pieza Indeterminate, como se detalla a continuación.

El enfoque anterior funciona bien, pero se siente artificial. Especialmente por lo que esta parte:

class Indeterminate a where 
    indeterminate :: a 

data T = T 

instance Indeterminate T where 
    indeterminate = T 

data S = S 

instance Indeterminate S where 
    indeterminate = S 

(y así sucesivamente para tal vez un poco más indeterminado). Se siente raro e incorrecto. Básicamente, estoy tratando de exigir que las instancias de Indeterminate sean singletons (en this sense). La sensación de rareza es un indicador de que podría estar atacando esto erróneamente. Otro es el hecho de que termino teniendo que anotar muchos de mis Polynomial a b s ya que el tipo real b a menudo no se puede inferir (eso no es extraño, pero es molesto, sin embargo).

¿Alguna sugerencia? ¿Debo seguir haciéndolo así o me estoy perdiendo algo?

PD: No se ofenda si no voto de más ni acepto respuestas de inmediato. No podré volver a consultar durante unos días.

Answer 1

En primer lugar, no estoy seguro de esto:

data (Ring a, Indeterminate b) => Polynomial a b 

... está haciendo lo que se espera que lo haga. Los contextos en las definiciones data no son terriblemente útiles; consulte the discussion here por alguna razón, la mayoría de las cuales equivale a forzarlos a agregar anotaciones adicionales sin proporcionar muchas garantías de tipo adicionales.

En segundo lugar, ¿realmente le importa el parámetro "indeterminado" que no sea para garantizar que los tipos se mantengan distintos? Una forma bastante estándar de hacer ese tipo de cosas es lo que se llama phantom types --encialmente, parámetros en el constructor de tipos que no se usan en el constructor de datos. Que nunca uso o necesita un valor del tipo fantasma, por lo que las funciones pueden ser tan polimórfica como desee, por ejemplo:

data Foo a b = Foo b 

foo :: Foo a b -> Foo a b 
foo (Foo x) = Foo x 

bar :: Foo a c -> Foo b c 
bar (Foo x) = Foo x 

baz :: Foo Int Int -> Foo Char Int -> Foo() Int 
baz (Foo x) (Foo y) = Foo $ x + y 

Obviamente esto requiere anotaciones, pero sólo en los lugares donde se está añadiendo deliberadamente restricciones .De lo contrario, la inferencia funcionará normalmente para el parámetro de tipo fantasma.

Me parece que el enfoque anterior debería ser suficiente para lo que está haciendo aquí: el negocio con tipos de singleton consiste principalmente en cerrar la brecha entre cálculos de nivel de tipo más complicados y cálculos de nivel de valor regulares creando escriba proxies para valores. Esto podría ser útil para, por ejemplo, marcar vectores con tipos que indiquen su base o marcar valores numéricos con unidades físicas, ambos casos donde la anotación tiene más significado que solo "una indeterminada llamada X".