online - Demostrando que "no hay corrupción" en Haskell

haskell pdf

Question

Trabajo en una industria crítica para la seguridad, y nuestros proyectos de software generalmente tienen requisitos de seguridad impuestos; cosas que tenemos que demostrar que el software hace con un alto grado de certeza. A menudo, estos son negativos, como "no se corromperá con más frecuencia que 1 en". (Debo añadir que estos requisitos provienen de los requisitos de seguridad del sistema estadístico).

Una fuente de corrupción es claramente los errores de codificación, y me gustaría usar el sistema de tipo Haskell para excluir al menos algunas clases de estos errores. Algo como esto:

Primero, aquí está nuestro elemento de datos críticos que no debe estar dañado.

newtype Critical = Critical String

Ahora quiero almacenar este artículo en algunas otras estructuras.

data Foo = Foo Integer Critical
data Bar = Bar String Critical

Ahora quiero escribir una función de conversión de Foo a Bar que garantice no desordenar los datos críticos.

goodConvert, badConvert :: Foo -> Bar
goodConvert (Foo n c) = Bar (show n) c
badConvert (Foo n (Critical s)) = Bar (show n) (Critical $ "Bzzt - " ++ s)

Quiero que "goodConvert" escriba "check", pero "badConvert" falla el chequeo de tipo.

Obviamente, no puedo importar con cuidado el constructor Crítico en el módulo que realiza la conversión. Pero sería mucho mejor si pudiera expresar esta propiedad en el tipo, porque entonces puedo componer funciones que están garantizadas para preservar esta propiedad.

He intentado agregar tipos fantasma y "forall" en varios lugares, pero eso no ayuda.

Una cosa que funcionaría sería no exportar el constructor Crítico, y luego tener

mkCritical :: String -> IO Critical

Dado que el único lugar donde se crean estos elementos de datos críticos es en las funciones de entrada, esto tiene cierto sentido. Pero prefiero una solución más elegante y general.

Editar

En los comentarios, FUZxxl sugirió un vistazo a Safe Haskell . Esto parece la mejor solución. En lugar de agregar un modificador "sin daños" en el nivel de tipo que originalmente quería, parece que puedes hacerlo a nivel de módulo, de esta forma:

1: Cree un módulo "Crítico" que exporte todas las características del tipo de datos Crítico, incluido su constructor. Marque este módulo como "inseguro" colocando "{- # LANGUAGE Insafe # -}" en el encabezado.

2: Cree un módulo "SafeCritical" que re-exporte todo excepto el constructor y cualquier otra función que pueda usarse para corromper un valor crítico. Marque este módulo como "confiable".

3: Marque todos los módulos necesarios para manejar los valores críticos sin corrupción como "seguros". Luego, use esto para demostrar que cualquier función importada como "segura" no puede causar daños en un valor Crítico.

Esto dejará una minoría más pequeña de código, como el código de entrada que analiza los valores críticos y requiere una verificación adicional. No podemos eliminar este código, pero reducir la cantidad que necesita verificación detallada sigue siendo una ganancia importante.

El método se basa en el hecho de que una función no puede inventar un nuevo valor a menos que una función lo devuelva. Si una función solo obtiene un valor Crítico (como en la función "convertir" anterior), ese es el único que puede devolver.

Una variación más difícil del problema se produce cuando una función tiene dos o más valores críticos del mismo tipo; Tiene que garantizar que no se mezclan. Por ejemplo,

swapFooBar :: (Foo, Bar) -> (Bar, Foo)
swapFooBar (Foo n c1, Bar s c2) = (Bar s c1, Foo n c2)

Sin embargo, esto puede manejarse dando el mismo tratamiento a las estructuras de datos que lo contienen.

Answer 1

Creo que la solución de ocultar constructores es idiomática. Puede exportar dos funciones:

mkCritical :: String -> D Critical
extract :: Critical -> String

donde D es la mónada trivial , o cualquier otra. Cualquier función que crea objetos de tipo Critical en algún punto está marcada con D Una función sin esa D puede extraer datos de objetos Critical , pero no crear nuevos.

Alternativamente:

data C a = C a Critical
modify :: (a -> String -> b) -> C a -> C b
modify f (C x (Critical y)) = C (f x y) (Critical y)

Si no exporta el constructor C , solo modify , puede escribir:

goodConvert :: C Int -> C String
goodConvert = modify (/(a, _) -> show a)

Pero badConvert es imposible de escribir.

Answer 2

Puedes usar parametricidad para llegar hasta allí.

data Foo c = Foo Integer c
data Bar c = Bar String c
goodConvert :: Foo c -> Bar c
goodConvert (Foo n c) = Bar (show n) c

Dado que c es una variable de tipo sin restricciones, usted sabe que la función goodConvert no puede saber nada sobre c , y por lo tanto no puede construir un valor diferente de ese tipo. Tiene que usar el proporcionado en la entrada.

Bueno, casi. Los valores de fondo le permiten romper esta garantía. Sin embargo, al menos sabe que si intenta usar un valor "dañado", se producirá una excepción (o no terminación).

badConvert :: Foo c -> Bar c
badConvert (Foo n c) = Bar (show n) undefined

Answer 3

Si bien la solución de Hammar es excelente y normalmente sugeriría constructores inteligentes / no exportar el constructor, hoy decidí intentar resolver esto en el asistente de pruebas de Coq y extraerlo a Haskell.

¡Tomar nota! No estoy muy versado en Coq / extracción. Algunas personas han hecho un buen trabajo probando y extrayendo el código de Haskell, así que busque ejemplos de calidad. ¡Estoy jugando!

Primero queremos definir sus tipos de datos. En Coq, esto se parece mucho a Haskell GADTs:

Require Import String.
Require Import ZArith.
Inductive Critical :=
Crit : string -> Critical.
Inductive FooT :=
Foo : Z -> Critical -> FooT.
Inductive BarT :=
Bar : string -> Critical -> BarT.

Piensa en esas líneas Inductive , como Inductive FooT := Foo : ... . , como declaraciones de tipo de datos: data FooT = Foo Integer Critical

Para facilitar su uso, vamos a obtener algunos accesores de campo:

Definition critF f := match f with Foo _ c => c end.
Definition critB b := match b with Bar _ c => c end.

Como Coq no define muchas funciones de estilo "mostrar", usaré un marcador de posición para mostrar enteros.

Definition ascii_of_Z (z : Z) : string := EmptyString. (* FIXME *)

Ahora tenemos lo básico, definamos la función goodConvert !

Definition goodConvert (foo : FooT) : BarT :=
match foo with
Foo n c => Bar (ascii_of_Z n) c
end.

Todo esto es bastante obvio: es su función de conversión, pero en Coq y usar un case como una declaración en lugar de una coincidencia de patrones de nivel superior. Pero, ¿cómo sabemos que esta función realmente va a mantener el invariante? ¡Lo demostramos!

Lemma convertIsGood : forall (f : FooT) (b : BarT),
goodConvert f = b -> critF f = critB b.
Proof.
intros.
destruct f. destruct b.
unfold goodConvert in H. simpl.
inversion H. reflexivity.
Qed.

Eso dice que si la conversión de f resulta en b entonces el campo crítico de f debe ser el mismo que el campo crítico de b (asumiendo algunas cosas menores, como no estropear las implementaciones de accesores de campo).

Ahora vamos a extraer esto a Haskell!

Extraction Language Haskell.
Extract Constant ascii_of_Z => "Prelude.show". (* obviously, all sorts of unsafe and incorrect behavior can be introduced by your extraction *)
Extract Inductive string => "Prelude.String" ["[]" ":"]. Print positive.
Extract Inductive positive => "Prelude.Integer" ["`Data.Bits.shiftL` 1 + 1" "`Data.Bits.shiftL` 1" "1"].
Extract Inductive Z => "Prelude.Integer" ["0" "" ""].
Extraction "so.hs" goodConvert critF critB.

Productor:

module So where
import qualified Prelude
data Bool =
True
| False
data Ascii0 =
Ascii Bool Bool Bool Bool Bool Bool Bool Bool
type Critical =
Prelude.String
-- singleton inductive, whose constructor was crit
data FooT =
Foo Prelude.Integer Critical
data BarT =
Bar Prelude.String Critical
critF :: FooT -> Critical
critF f =
case f of {
Foo z c -> c}
critB :: BarT -> Critical
critB b =
case b of {
Bar s c -> c}
ascii_of_Z :: Prelude.Integer -> Prelude.String
ascii_of_Z z =
[]
goodConvert :: FooT -> BarT
goodConvert foo =
case foo of {
Foo n c -> Bar (ascii_of_Z n) c}

¿Podemos correrlo? ¿Funciona?

> critB $ goodConvert (Foo 32 "hi")
"hi"

¡Estupendo! Si alguien tiene sugerencias para mí, aunque esta es una "respuesta", soy todo oídos. No estoy seguro de cómo eliminar el código muerto de cosas como Ascii0 o Bool , por no mencionar las buenas instancias de los shows. Si alguien tiene curiosidad, creo que los nombres de los campos se pueden hacer automáticamente si utilizo un Record lugar de un Inductive , pero eso podría hacer que esta publicación sea más fea sintácticamente.