Como posso usar evidências contraditórias?
Enquanto escreviasobre como fazer a subtipagem em Haskell, ocorreu-me que seria muito conveniente poder "usar" evidências contraditórias, comoTrue ~ False
para informar o compilador sobre ramificações mortas. Com outro tipo vazio padrão,Void
, aEmptyCase
A extensão permite marcar um ramo morto (ou seja, um que contenha um valor do tipoVoid
) deste jeito:
use :: Void -> a
use x = case x of
Eu gostaria de fazer algo semelhante por insatisfatórioConstraint
s.
Existe um termo que pode receber o tipoTrue ~ False => a
mas não pode receber o tipoa
?