Qual é o objetivo pretendido doSo tipo? Transliterando para o Agda:

data So : Bool → Set where
  oh : So true

So eleva uma proposição booleana até uma proposição lógica. Artigo introdutório de Oury e SwierstraO poder do Pi fornece um exemplo de álgebra relacional indexada pelas colunas das tabelas. Tomar o produto de duas tabelas requer que elas tenham colunas diferentes, para as quais elas usamSo:

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')

Estou acostumado a construir termos de evidência para as coisas que quero provar sobre meus programas. Parece mais natural construir uma relação lógica emSchemas para garantir a desarticulação:

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

So parece ter sérias desvantagens em comparação com um termo de prova "adequado": correspondência de padrões emoh não fornece nenhuma informação com a qual você poderia fazer outro termo de verificação de tipo (dá?) - o que significariaSo os valores não podem participar de forma proveitosa da prova interativa. Compare isso com a utilidade computacional deDisjoint, que é representado como uma lista de provas de que cada coluna ems' não aparece ems.

Eu realmente não acredito que a especificaçãoSo (disjoint s s') é mais simples de escrever do queDisjoint s s' - você precisa definir o valor booleanodisjoint funcionar sem a ajuda do verificador de tipo - e em qualquer casoDisjoint se paga quando você deseja manipular as evidências nele contidas.

Eu também sou cético queSo economiza esforço quando você está construindo umProduct. Para dar um valor deSo (disjoint s s'), você ainda precisa fazer a correspondência de padrões suficiente ems es' para satisfazer o verificador de tipo de que eles são de fato disjuntos. Parece um desperdício descartar as evidências assim geradas.

So parece difícil para autores e usuários do código no qual ele é implantado. "Então", em que circunstâncias eu gostaria de usarSo?