¿Cómo funciona el paquete de restricciones?

La idea detrás de Data.Constraint.Forall, según tengo entendido, es utilizar la coerción en la implementación, pero garantizar la seguridad mediante el sistema de tipos. Tengo dos preguntas con respecto a este último.¿Cómo funciona el paquete de restricciones?

¿Por qué necesitamos dos variables skolem - A y B? Me imagino que si una restricción es satisfecha por un tipo "desconocido", entonces es polimórfica. ¿Cómo el segundo tipo da más seguridad?
¿Por qué estos tipos se llaman variables skolem? Pensé que la skolemnización se usa para eliminar la cuantificación existencial, y aquí vemos la cuantificación universal. ¿Hay algún cambio de signo en alguna parte que me haya perdido?

Fuente

2012-10-04 Roman Cheplyaka

Es posible con un MPTC y una dependencia funcional identificar el Skolem cuando es una sola variable, mediante el uso de una restricción parametrizada en una restricción. El truco que solía hacer eso no funciona cuando hay dos.

Desde la perspectiva del código escrito fuera de este módulo, las variables son Skolemized. En realidad, son un constructor de tipo 'fresco'.

Pero dado que no se puede hacer referencia explícitamente a estos tipos fuera del módulo ya que no se exportan, cualquier instancia que cubra estos Skolems tiene que ser universalmente cuantificada.

Así es como me actualizo de lo existencial a lo universal. El 'cambio de signo' proviene de su naturaleza no extraída, no técnicamente de su papel como Skolems.

Fuente

2012-10-04 15:19:05

Gracias. ¿Podrías mostrar el truco del que estás hablando? Además, ¿tiene usted una prueba (o un argumento convincente) de que dos variables son suficientes? –

Veré si puedo desenterrarlo. Fue solo un ejemplo rápido que me golpeé cuando escribí el código en cuestión. El "argumento convincente" es que el truco con el que se me ocurrió no funcionó, y que cualquier boceto que se me ocurriera y que pudiera verse a través de él iba a ser demasiado trabajo para probar. Puede ser posible con suficiente Oleggery para solucionar las dos soluciones variables, pero seguramente necesitará una maquinaria bastante pesada para hacerlo. ;) –

Fuera del manguito, el ejemplo más simple se reducía al uso de una clase y un fundep. Recuerde que puede tener 'clase Foo a b | a -> b, b -> a', luego si 'cuantifica' sobre el segundo argumento de 'Foo a a' no es paramétrico en su segundo argumento, aunque puede instanciar ese segundo argumento con Skolem 'A'. Pero cuando vas a usar dos tipos, el truco de fundep ya no funciona, porque ahora el requisito para ambos '(Foo A A, Foo A B)' vence al fundep. –

¿Cómo funciona el paquete de restricciones?

Respuesta

Cuestiones relacionadas