haskell - tabla - Probar la idempotencia de la disyunción a nivel de tipo

leyes logicas

Question

He definido la disyunción a nivel de tipo de la siguiente manera:

{-# LANGUAGE DataKinds, TypeFamilies #-}
type family Or (a :: Bool) (b :: Bool) :: Bool
type instance Or False a = a
type instance Or True a = True

Ahora me gustaría probar (en Haskell) que es idempotente. Es decir, quiero construir un término idemp con tipo

idemp :: a ~ b => proxy (Or a b) -> proxy a

que es operativamente equivalente a id . (Obviamente, puedo definirlo, por ejemplo, como unsafeCoerce , pero eso es hacer trampa).

¿Es posible?

Answer 1

Como dice John L en su comentario, actualmente no hay manera de hacer esto sin restricciones adicionales, que yo sepa. No puede explotar el hecho de que Bool es un tipo cerrado en el nivel de término, y no hay manera de hacer un análisis de caso en la variable de tipo de tipo Bool en idemp .

La solución típica es reflejar la estructura de tipo Bool en el nivel de término utilizando tipos singleton:

data SBool :: Bool -> * where
SFalse :: SBool False
STrue :: SBool True

Para cualquier b :: Bool , solo hay un habitante de SBool b (módulo undefined , por supuesto).

Con SBool , el teorema es fácil de probar (no sé por qué agregó la restricción de igualdad adicional, lo eliminaré):

idemp'' :: SBool a -> proxy (Or a a) -> proxy a
idemp'' SFalse x = x
idemp'' STrue x = x

En lugar de pasar el argumento explícitamente, puede pasarlo implícitamente, definiendo una clase que pueda crear la representación de SBool :

class CBool (b :: Bool) where
sBool :: SBool b
instance CBool True where sBool = STrue
instance CBool False where sBool = SFalse

Entonces:

idemp :: CBool a => proxy (Or a a) -> proxy a
idemp = idemp'' sBool

No creo que puedas deshacerte de la restricción CBool , pero es trivialmente cierto para cualquier a :: Bool , así que no es una suposición muy fuerte.

Answer 2

Lo que pides no es posible, pero algo como lo podría hacer en su lugar. No es posible porque la prueba requiere un análisis de caso en Booleans de nivel de tipo, pero no tiene datos que le permitan hacer que ocurra tal evento. La solución es incluir solo esa información a través de un singleton.

Primero, déjeme notar que su tipo para idemp es un poco idemp . La restricción a ~ b solo nombra lo mismo dos veces. Las siguientes comprobaciones de tipo:

idemq :: p (Or b b) -> p b
idemq = undefined
idemp :: a ~ b => p (Or a b) -> p a
idemp = idemq

(Si tiene una restricción a ~ t donde t no contiene a , generalmente es bueno sustituir t por a . La excepción está en las declaraciones de instance : una a en una cabeza de instancia coincidirá con cualquier cosa, por lo tanto, la instancia se activará incluso si La cosa aún no se ha convertido obviamente en t . Pero estoy divagando.)

idemq que idemq es indefinible porque no tenemos información útil sobre b . Los únicos datos disponibles habitan p -de-algo, y no sabemos qué es p .

Necesitamos razonar por casos en b . Tenga en cuenta que con las familias de tipos recursivas generales, podemos definir valores booleanos de nivel de tipo que no sean True ni False . Si UndecidableInstances , puedo definir

type family Loop (b :: Bool) :: Bool
type instance Loop True = Loop False
type instance Loop False = Loop True

por lo tanto, Loop True no se puede reducir a True o False , y, peor en el ámbito local, no hay manera de demostrar que

Or (Loop True) (Loop True) ~ Loop True -- this ain''t so

No hay forma de salir de esto. Necesitamos evidencia de tiempo de ejecución de que nuestro b es uno de los booleanos de buen comportamiento que de alguna manera calcula un valor. Cantemos pues

data Booly :: Bool -> * where
Truey :: Booly True
Falsey :: Booly False

Si conocemos Booly b , podemos hacer un análisis de caso que nos dirá qué es b . Cada caso entonces pasará muy bien. Así es como lo jugaría, usando un tipo de igualdad definido con PolyKinds para empacar los hechos, en lugar de abstraer sobre usos pb .

data (:=:) a b where
Refl :: a :=: a

Nuestro hecho clave ahora está claramente establecido y probado:

orIdem :: Booly b -> Or b b :=: b
orIdem Truey = Refl
orIdem Falsey = Refl

Y podemos implementar este hecho mediante un análisis estricto de casos:

idemp :: Booly b -> p (Or b b) -> p b
idemp b p = case orIdem b of Refl -> p

El análisis del caso debe ser estricto, para verificar que la evidencia no es una mentira descabellada, sino más bien un Refl honesto de la bondad. Refl silencio la prueba de Or bb ~ b que se necesita para arreglar los tipos.

Si no desea agrupar explícitamente todos estos valores singleton, puede, como sugiere kosmikus, esconderlos en un diccionario y extraerlos cuando los necesite.

Richard Eisenberg y Stephanie Weirich tienen una biblioteca Template Haskell que reúne estas familias y clases para ti. SHE puede construirlos también y te permite escribir.

orIdem pi b :: Bool. Or b b :=: b
orIdem {True} = Refl
orIdem {False} = Refl

donde pi b :: Bool. Se expande a forall b :: Bool. Booly b -> forall b :: Bool. Booly b -> .

Pero es una palabrería. Es por eso que mi pandilla está trabajando en agregar un pi real a Haskell, ya que es un cuantificador no paramétrico (distinto de forall y -> ) que puede ser instanciado por cosas en la intersección ahora no trivial entre los lenguajes de tipos y términos de Haskell. Esta pi también podría tener una variante "implícita", donde el argumento se mantiene oculto por defecto. Los dos respectivamente corresponden al uso de familias y clases singleton, pero no es necesario definir tipos de datos tres veces para obtener el kit adicional.

Podría valer la pena mencionar que en una teoría de tipos total, no es necesario pasar la copia adicional de Boolean b en tiempo de ejecución. La cosa es que, b se usa solo para probar que los datos pueden ser transportados de p (Or bb) a pb , no necesariamente para hacer que los datos sean transportados. No calculamos bajo carpetas en tiempo de ejecución, por lo que no hay forma de preparar una prueba deshonesta de la ecuación, por lo tanto, podemos borrar el componente de prueba y la copia de b que lo entrega. Como dice Randy Pollack, lo mejor de trabajar en un cálculo fuertemente normalizado es no tener que normalizar las cosas .