¿Cuál es el propósito previsto de laSo ¿tipo? Transliterando a Agda:

data So : Bool → Set where
  oh : So true

So eleva una proposición booleana a una lógica. Documento introductorio de Oury y SwierstraEl poder de pi da un ejemplo de álgebra relacional indexada por las columnas de las tablas. Tomar el producto de dos tablas requiere que tengan columnas diferentes, para lo cual usanSo:

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 sobre mis programas. Parece más natural construir una relación lógica sobreSchemas para garantizar la desarticulación:

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

So parece tener serias desventajas en comparación con un término de prueba "adecuado": coincidencia de patrones enoh no le da ninguna información con la que pueda hacer otro término de verificación de tipo (¿lo hace?), lo que significaríaSo los valores no pueden participar útilmente en la prueba interactiva. Compare esto con la utilidad computacional deDisjoint, que se representa como una lista de pruebas de que cada columna ens' no aparece ens.

Realmente no creo que la especificaciónSo (disjoint s s') es más sencillo de escribir queDisjoint s s' - tienes que definir el booleanodisjoint funciona sin ayuda del verificador de tipos, y en cualquier casoDisjoint se paga solo cuando desea manipular la evidencia contenida en el mismo.

También soy escéptico de queSo ahorra esfuerzo cuando estás construyendo unProduct. Para dar un valor deSo (disjoint s s'), todavía tiene que hacer suficiente coincidencia de patrones ens ys' para satisfacer al verificador de tipo que de hecho son disjuntos. Parece un desperdicio descartar la evidencia así generada.

So Parece difícil de manejar tanto para los autores como para los usuarios del código en el que se implementa. 'Entonces', ¿bajo qué circunstancias me gustaría usarSo?