haskell - ¿Se pueden usar GADT para probar las desigualdades tipo en GHC?

curry-howard

Question

Entonces, en mis intentos continuos de entender a medias a Curry-Howard a través de pequeños ejercicios de Haskell, me he quedado atascado en este punto:

{-# LANGUAGE GADTs #-}

import Data.Void

type Not a = a -> Void

-- | The type of type equality proofs, which can only be instantiated if a = b.
data Equal a b where
    Refl :: Equal a a

-- | Derive a contradiction from a putative proof of @Equal Int Char@.
intIsNotChar :: Not (Equal Int Char)
intIsNotChar intIsChar = ???

Claramente, el tipo Equal Int Char no tiene habitantes (no inferiores), y semánticamente debería haber un absurdEquality :: Equal Int Char -> a función ... pero por mi vida no puedo entender de ninguna manera escribir uno que no sea undefined

Entonces o bien:

1. Me falta algo, o
2. Hay una cierta limitación del lenguaje que hace que esta sea una tarea imposible, y no he logrado entender de qué se trata.

Sospecho que la respuesta es algo como esto: el compilador no puede explotar el hecho de que no hay constructores Equal que no tengan a = b. Pero si eso es así, ¿qué lo hace verdad?

Answer 1

Aquí hay una versión más corta de la solución de Philip JF, que es la forma en que los teóricos del tipo dependiente han estado refutando ecuaciones durante años.

type family Discriminate x
type instance Discriminate Int  = ()
type instance Discriminate Char = Void

transport :: Equal a b -> Discriminate a -> Discriminate b
transport Refl d = d

refute :: Equal Int Char -> Void
refute q = transport q ()

Para mostrar que las cosas son diferentes, debes observar que se comportan de manera diferente al proporcionar un contexto computacional que da como resultado observaciones distintas. Discriminate proporciona exactamente ese contexto: un programa de nivel de tipo que trata los dos tipos de manera diferente.

No es necesario recurrir a undefined para resolver este problema. La programación total a veces implica rechazar las entradas imposibles. Incluso cuando undefined esté disponible, recomendaría no usarlo cuando sea suficiente un método total: el método total explica por qué algo es imposible y el registrador de tipos confirma; undefined meramente documenta su promesa . De hecho, este método de refutación es cómo Epigram prescinde de "casos imposibles" al tiempo que garantiza que el análisis de un caso cubre su dominio.

En cuanto al comportamiento computacional, nótese que refute , a través del transport es necesariamente estricto en q que q no puede computar encabezar la forma normal en el contexto vacío, simplemente porque no existe esa forma normal (y porque la computación conserva el tipo, por supuesto). En una configuración total, nos aseguraríamos de que nunca se invocaría refute en tiempo de ejecución. En Haskell, al menos estamos seguros de que su argumento divergerá o arrojará una excepción antes de que tengamos que responder. Una versión perezosa , como

absurdEquality e = error "you have a type error likely to cause big problems"

ignorará la toxicidad de e y le dirá que tiene un error tipográfico cuando no lo haga. yo prefiero

absurdEquality e = e `seq` error "sue me if this happens"

si la refutación honesta es demasiado trabajo duro.

Answer 2

No entiendo el problema con el uso undefined cada tipo está habitado por abajo en Haskell. Nuestro lenguaje no está fuertemente normalizado ... Estás buscando algo equivocado. Equal Int Char conduce a errores de tipo no muy bien conservadas excepciones. Ver

{-# LANGUAGE GADTs, TypeFamilies #-}

data Equal a b where
    Refl :: Equal a a

type family Pick cond a b
type instance Pick Char a b = a
type instance Pick Int a b = b

newtype Picker cond a b = Picker (Pick cond a b)

pick :: b -> Picker Int a b
pick = Picker

unpick :: Picker Char a b -> a
unpick (Picker x) = x

samePicker :: Equal t1 t2 -> Picker t1 a b -> Picker t2 a b
samePicker Refl x = x

absurdCoerce :: Equal Int Char -> a -> b
absurdCoerce e x = unpick (samePicker e (pick x))

podrías usar esto para crear la función que quieras

absurdEquality e = absurdCoerce e ()

pero eso producirá un comportamiento indefinido como regla de cálculo. false debería hacer que los programas aborten, o al menos se ejecuten para siempre. Abortar es la regla de cálculo que es similar a convertir la lógica mínima en lógica intuitiva agregando no. La definición correcta es

absurdEquality e = error "you have a type error likely to cause big problems"

en cuanto a la pregunta en el título: esencialmente no. Según mi leal saber y entender, la desigualdad tipo no es representable de manera práctica en el Haskell actual. Los cambios que se avecinan en el sistema de tipos pueden hacer que esto sea cada vez más agradable, pero a partir de ahora, tenemos igualdades pero no desigualdades.