Eventuali trucchi per sbarazzarsi di boilerplate quando si costruiscono prove di assurdo predicato sulle enumerazioni?

Question

Diciamo che ho

data Fruit = Apple | Banana | Grape | Orange | Lemon | {- many others -} 

e un predicato su quel tipo,

data WineStock : Fruit -> Type where 
    CanonicalWine : WineStock Grape 
    CiderIsWineToo : WineStock Apple 

che non detiene per Banana, Orange, Lemon e altri.

E 'can be said che questo definisce WineStock come un predicato su Fruit; WineStock Grape è vero (dal momento che siamo in grado di costruire un valore/prova di questo tipo: CanonicalWine), così come WineStock Apple, ma WineStock Banana è falso, dal momento che il tipo non è abitata da eventuali valori/prove.

---

Poi, come posso andare su come utilizzare in modo efficace Not (WineStock Banana), Not (WineStock Lemon), ecc? Sembra che per ogni costruttore Fruit oltre Grape e Apple, non posso fare a meno di codificare un caso suddiviso su WineStock, da qualche parte, pieno di impossible s:

instance Uninhabited (WineStock Banana) where 
    uninhabited CanonicalWine impossible 
    uninhabited CiderIsWineToo impossible 

instance Uninhabited (WineStock Lemon) where 
    uninhabited CanonicalWine impossible 
    uninhabited CiderIsWineToo impossible 

instance Uninhabited (WineStock Orange) where 
    uninhabited CanonicalWine impossible 
    uninhabited CiderIsWineToo impossible 

Nota che:

• il codice è ripetitivo,
• LoC esploderà quando la definizione del predicato aumenta, acquisendo più costruttori. Immagina solo la prova Not (Sweet Lemon), supponendo che ci siano molte alternative dolci nella definizione Fruit.

Quindi, in questo modo non del tutto soddisfacente sembra, quasi impraticabile .

Ci sono approcci più eleganti?

Answer 1

@slcv ha ragione: usare una funzione che calcola se un frutto soddisfa una proprietà o no piuttosto che costruire vari predicati induttivi ti permetterà di sbarazzarti di questo sovraccarico.

Qui è la configurazione minima:

data Is : (p : a -> Bool) -> a -> Type where 
    Indeed : p x = True -> Is p x 

isnt : {auto eqF : p a = False} -> Is p a -> b 
isnt {eqF} (Indeed eqT) = case trans (sym eqF) eqT of 
          Refl impossible 

Is p x assicura che la proprietà p tiene dell'elemento x (ho usato un tipo induttivo piuttosto che un tipo alias in modo che Idris non si sviluppa nel contesto di un buco, è più facile da leggere in questo modo).

isnt prf respinto la prova fasulla prf ogniqualvolta controllore dei tipi è in grado di generare una prova che p a = False automaticamente (tramite Refl o assunzione nel contesto).

Una volta che avete questi, è possibile iniziare a definire le vostre proprietà da solo enumerando i casi positivi e l'aggiunta di un ripostiglio

wineFruit : Fruit -> Bool 
wineFruit Grape = True 
wineFruit Apple = True 
wineFruit _  = False 

weaponFruit : Fruit -> Bool 
weaponFruit Apple = True 
weaponFruit Orange = True 
weaponFruit Lemon = True 
weaponFruit _  = False 

È possibile definire i predicati originali di tipo alias chiamata Is con la funzione di decisione appropriata:

WineStock : Fruit -> Type 
WineStock = Is wineFruit 

E, abbastanza sicuro, isnt consente di respingere i casi impossibili:

dismiss : WineStock Orange -> Void 
dismiss = isnt