instalar - haskell ejemplos

¿Es posible programar y verificar invariantes en Haskell?

Question

Cuando escribo un algoritmo, generalmente escribo invariantes en los comentarios.

Por ejemplo, una función puede devolver una lista ordenada, y la otra espera que se ordene una lista.
Soy consciente de que los probadores de teoremas existen, pero no tengo experiencia en usarlos.

También creo que el compilador inteligente [sic!] Puede hacer uso de ellos para optimizar el programa.
Entonces, ¿es posible anotar invariantes y hacer que el compilador los revise?

Answer 1

Bueno, la respuesta es si o no. No hay manera de escribir un invariante separado de un tipo y verificarlo. Sin embargo, hubo una implementación de esto en una bifurcación de investigación de Haskell llamada ESC / Haskell: http://lambda-the-ultimate.org/node/1689

Tienes varias otras opciones Por un lado, puede usar aserciones: http://www.haskell.org/ghc/docs/7.0.2/html/users_guide/assertions.html

Luego, con la marca correspondiente, puede desactivar estas aserciones para la producción.

Más generalmente, puedes codificar los invariantes en tus tipos. Iba a agregar más aquí, pero Dons me derrotó a los tiradores.

Un ejemplo más es esta muy buena codificación de árboles rojo-negros: http://www.reddit.com/r/haskell/comments/ti5il/redblack_trees_in_haskell_using_gadts_existential/

Answer 2

El siguiente es un truco, pero es un truco bastante seguro, así que inténtalo en casa. Utiliza algunos de los entretenidos juguetes nuevos para hornear invariantes de orden en mergeSort.

{-# LANGUAGE GADTs, PolyKinds, KindSignatures, MultiParamTypeClasses,
    FlexibleInstances, RankNTypes, FlexibleContexts #-}

Tendré números naturales, solo para mantener las cosas simples.

data Nat = Z | S Nat deriving (Show, Eq, Ord)

Pero definiré <= en la clase de tipos Prolog, para que el buscador de tipos pueda tratar de averiguar el orden implícitamente.

class LeN (m :: Nat) (n :: Nat) where
instance             LeN Z n where
instance LeN m n =>  LeN (S m) (S n) where

Para ordenar los números, necesito saber que cualquiera de los dos números se puede ordenar de una forma u otra . Digamos lo que significa que dos números sean tan fáciles de ordenar.

data OWOTO :: Nat -> Nat -> * where
  LE :: LeN x y => OWOTO x y
  GE :: LeN y x => OWOTO x y

Nos gustaría saber que cada dos números pueden ordenarse, siempre que tengamos una representación de ellos en tiempo de ejecución. En estos días, conseguimos eso construyendo la familia singleton para Nat . Natty n es el tipo de copias en tiempo de ejecución de n .

data Natty :: Nat -> * where
  Zy :: Natty Z
  Sy :: Natty n -> Natty (S n)

La comprobación de la forma en que se encuentran los números es muy parecida a la versión booleana habitual, excepto con pruebas. El caso paso requiere desempaquetado y reembalaje porque los tipos cambian. La inferencia de instancias es buena para la lógica involucrada.

owoto :: forall m n. Natty m -> Natty n -> OWOTO m n
owoto Zy      n       = LE
owoto (Sy m)  Zy      = GE
owoto (Sy m)  (Sy n)  = case owoto m n of
  LE -> LE
  GE -> GE

Ahora que sabemos cómo poner los números en orden, veamos cómo hacer listas ordenadas. El plan es describir lo que es estar en orden entre límites . Por supuesto, no queremos excluir ningún elemento que se pueda ordenar, por lo que el tipo de límites amplía el tipo de elemento con los elementos superior e inferior.

data Bound x = Bot | Val x | Top deriving (Show, Eq, Ord)

Extiendo la noción de <= consecuencia, para que el buscador de tipos pueda hacer la verificación de límites.

class LeB (a :: Bound Nat)(b :: Bound Nat) where
instance             LeB Bot     b        where
instance LeN x y =>  LeB (Val x) (Val y)  where
instance             LeB (Val x) Top      where
instance             LeB Top     Top      where

Y aquí hay listas ordenadas de números: una OList lu es una secuencia x1 :< x2 :< ... :< xn :< ONil tal que l <= x1 <= x2 <= ... <= xn <= u . La x :< verifica que x esté por encima del límite inferior, luego impone x como el límite inferior en la cola.

data OList :: Bound Nat -> Bound Nat -> * where
  ONil :: LeB l u => OList l u
  (:<) :: forall l x u. LeB l (Val x) =>
          Natty x -> OList (Val x) u -> OList l u

Podemos escribir merge para listas ordenadas de la misma manera que lo haríamos si fueran ordinarios. La clave invariante es que si ambas listas comparten los mismos límites, también lo hacen su combinación.

merge :: OList l u -> OList l u -> OList l u
merge ONil      lu         = lu
merge lu        ONil       = lu
merge (x :< xu) (y :< yu)  = case owoto x y of
  LE  -> x :< merge xu (y :< yu)
  GE  -> y :< merge (x :< xu) yu

Las ramas del análisis de casos extienden lo que ya se conoce a partir de las entradas con información de orden justa para satisfacer los requisitos de los resultados. La inferencia de instancias actúa como un generador de teoremas básicos: afortunadamente (o más bien, con un poco de práctica) las obligaciones de prueba son bastante fáciles.

Vamos a sellar el trato. Necesitamos construir testigos de tiempo de ejecución para los números con el fin de ordenarlos de esta manera.

data NATTY :: * where
  Nat :: Natty n -> NATTY

natty :: Nat -> NATTY
natty Z      =                           Nat Zy
natty (S n)  = case natty n of Nat n ->  Nat (Sy n)

Debemos confiar en que esta traducción nos da la NATTY que corresponde a la Nat que queremos ordenar. Esta interacción entre Nat , Natty y NATTY es un poco frustrante, pero eso es lo que se necesita en Haskell ahora. Una vez que tengamos eso, podemos construir la forma habitual de dividir y conquistar.

deal :: [x] -> ([x], [x])
deal []        = ([], [])
deal (x : xs)  = (x : zs, ys) where (ys, zs) = deal xs

sort :: [Nat] -> OList Bot Top
sort []   = ONil
sort [n]  = case natty n of Nat n -> n :< ONil
sort xs   = merge (sort ys) (sort zs) where (ys, zs) = deal xs

A menudo me sorprende la cantidad de programas que tienen sentido para nosotros y también lo es para un verificador de tipos.

[Aquí hay un kit de repuesto que construí para ver qué estaba pasando.

instance Show (Natty n) where
  show Zy = "Zy"
  show (Sy n) = "(Sy " ++ show n ++ ")"
instance Show (OList l u) where
  show ONil = "ONil"
  show (x :< xs) = show x ++ " :< " ++ show xs
ni :: Int -> Nat
ni 0 = Z
ni x = S (ni (x - 1))

Y nada estaba escondido.]

Answer 3

Las otras respuestas aquí son todas fabulosas, pero a pesar de que su pregunta mencionó específicamente la verificación del compilador, siento que esta página estaría incompleta sin al menos una sugerencia de QuickCheck . QuickCheck realiza su trabajo en tiempo de ejecución en lugar de en el sistema de tipos en tiempo de compilación, pero es una gran herramienta para probar propiedades que pueden ser demasiado difíciles o inconvenientes para expresarse estáticamente en el sistema de tipos.

Answer 4

Sí.

Codificas tus invariantes en el sistema de tipos Haskell. Luego, el compilador ejecutará (por ejemplo, realizar la comprobación de tipos), para evitar que su programa se compile si no se mantienen las invariantes.

Para listas ordenadas, podría considerar un enfoque barato de implementar un constructor inteligente que cambie el tipo de una lista al ordenar.

module Sorted (Sorted, sort) where

newtype Sorted a = Sorted { list :: [a] }

sort :: [a] -> Sorted a
sort = Sorted . List.sort

Ahora puede escribir funciones que asuman que Sorted está retenido, y el compilador evitará que pase cosas sin clasificar a esas funciones.

Puede ir mucho más allá y codificar propiedades extremadamente ricas en el sistema de tipos. Ejemplos:

• Acceso de matriz revisado estáticamente
• Acceso a la base de datos comprobada
• dimensiones físicas comprobadas

Con la práctica, el lenguaje puede imponer invariantes bastante sofisticados en el momento de la compilación.

Sin embargo, hay límites, ya que el sistema de tipos no está diseñado para probar las propiedades de los programas. Para pruebas de trabajo pesado, considere la verificación de modelos o el teorema de prueba de lenguajes como Coq. El lenguaje Agda es un lenguaje similar a Haskell cuyo sistema de tipos está destinado a demostrar propiedades ricas.