functional programming - shadowhunters - ¿Entonces cuál es el punto?

idris significado

Question

¿Cuál es el propósito del tipo So ? Transliterando en Agda:

data So : Bool → Set where
  oh : So true

So levanta una proposición booleana hasta una lógica. El documento introductorio de Oury y Swierstra, The Power of Pi, da un ejemplo de un álgebra relacional indexada por las columnas de las tablas. Tomar el producto de dos tablas requiere que tengan columnas diferentes, para las cuales usan So :

Schema = List (String × U)  -- U is the universe of SQL types

-- false iff the schemas share any column names
disjoint : Schema -> Schema -> Bool
disjoint = ...

data RA : Schema → Set where
  -- ...
  Product : ∀ {s s''} → {So (disjoint s s'')} → RA s → RA s'' → RA (append s s'')

Estoy acostumbrado a construir términos de evidencia para las cosas que quiero probar acerca de mis programas. Parece más natural construir una relación lógica en los Schema para asegurar la desunión:

Disjoint : Rel Schema _
Disjoint s s'' = All (λ x -> x ∉ cols s) (cols s'')
  where cols = map proj₁

Parece que tiene serias desventajas en comparación con un término de prueba "correcto": la coincidencia de patrones en oh no le proporciona ninguna información con la que pueda realizar otra verificación de tipo de término (¿lo hace?), Lo que significaría So valores pueden " Participa de manera útil en la prueba interactiva. Compare esto con la utilidad computacional de Disjoint , que se representa como una lista de pruebas de que cada columna en s'' no aparece en s .

Realmente no creo que la especificación So (disjoint s s'') es más simple de escribir que Disjoint s s'' , tiene que definir la función disjoint disjoint sin la ayuda del comprobador de tipos, y en cualquier caso, Disjoint paga sola cuando Quieres manipular la evidencia contenida en el mismo.

También soy escéptico de que So ahorra esfuerzo cuando estás construyendo un Product . Para dar un valor de So (disjoint s s'') , todavía tiene que hacer suficientes patrones de coincidencia en s y s'' para satisfacer el comprobador de tipos que, de hecho, son disjuntos. Parece un desperdicio desechar la evidencia así generada.

So parece difícil de manejar tanto para los autores como para los usuarios de código en el que se implementa. ''Entonces'', ¿bajo qué circunstancias querría usarlo?

Answer 1

Si ya tiene una b : Bool , puede convertirla en una proposición: So b , que es un poco más corto que b ≡ true . A veces (no recuerdo ningún caso real) no hay necesidad de molestarse con un tipo de datos adecuado, y esta solución rápida es suficiente.

So parece tener serias desventajas en comparación con un término de prueba "correcto": la coincidencia de patrones en oh no le proporciona ninguna información con la que pueda realizar otra verificación de tipo de término. Como corolario, los valores de So no pueden participar de manera útil en la prueba interactiva. Compare esto con la utilidad computacional de Disjoint , que se representa como una lista de pruebas de que cada columna en s'' no aparece en s .

Le proporciona la misma información que Disjoint , solo necesita extraerla. Básicamente, si no hay incoherencia entre disjoint y Disjoint , entonces debería ser capaz de escribir una función So (disjoint s) -> Disjoint s utilizando la coincidencia de patrones, la recursión y la eliminación de casos imposibles.

Sin embargo, si ajustas un poco la definición:

So : Bool -> Set
So true  = ⊤
So false = ⊥

So convierte en un tipo de datos realmente útil, porque x : So true se reduce a tt debido a la regla eta para ⊤ . Esto permite usar So como una restricción: en pseudo-Haskell podríamos escribir

forall n. (n <=? 3) => Vec A n

y si n está en forma canónica (es decir, suc (suc (suc ... zero)) ), entonces n <=? 3 n <=? 3 puede ser verificado por el compilador y no se necesitan pruebas. En Agda actual es

∀ {n} {_ : n <=? 3} -> Vec A n

Utilicé este truco en this respuesta (está {_ : False (m ≟ 0)} allí). Y supongo que sería imposible escribir una versión utilizable de la maquinaria descrita here sin esta simple definición:

Is-just : ∀ {α} {A : Set α} -> Maybe A -> Set
Is-just = T ∘ isJust

donde T es So en la biblioteca estándar de Agda.

Además, en presencia de argumentos de instancia, el tipo-as-a-data-type se puede usar como una restricción So -a-a:

open import Data.Bool.Base
open import Data.Nat.Base
open import Data.Vec

data So : Bool -> Set where
  oh : So true

instance
  oh-instance : So true
  oh-instance = oh

_<=_ : ℕ -> ℕ -> Bool
0     <= m     = true
suc n <= 0     = false
suc n <= suc m = n <= m

vec : ∀ {n} {{_ : So (n <= 3)}} -> Vec ℕ n
vec = replicate 0

ok : Vec ℕ 2
ok = vec

fail : Vec ℕ 4
fail = vec