2016-04-05 11 views
5

Ho provato a modellare una codifica monadica meno ingenua del non-determinismo (meno ingenuo di MonadPlus e liste comuni) in Coq che è spesso usato in Haskell; ad esempio la codifica per gli elenchi è simile aStrutture dati con componenti non deterministici in Coq

data List m a = Nil | Cons (m a) (m (List m a)) 

mentre la corrispondente definizione in Coq vorrebbe come segue.

Inductive List (M: Type -> Type) (A: Type) := 
    Nil: List M A 
| Cons : M A -> M (List M A) -> List M A. 

Tuttavia, questo tipo di definizione non è consentito in Coq a causa della Circostanza "strettamente positiva" per i tipi di dati induttivi.

Non sono sicuro di puntare a una risposta specifica di Coq oa un'implementazione alternativa in Haskell che posso formalizzare in Coq, ma sono felice di leggere qualsiasi suggerimento su come superare questo problema.

+2

Probabilmente siete alla ricerca di [ 'Freer'] (http://okmij.org/ ftp/Haskell/estensibile/more.pdf) monadi e l'effetto 'NDet' lì. Tutto è strettamente positivo e questa rappresentazione ti dà persino non-determinismo con [scelta impegnata] (http://okmij.org/ftp/papers/LogicT.pdf). Ho [implementato] (https://github.com/effectfully/Eff/blob/master/Simple/Effect/NonDet.agda) quello in Agda, ma il codice è orribile a causa del modo in cui Agda gestisce il polimorfismo dell'universo. – user3237465

+1

La scelta commessa (o la scelta del tempo di chiamata come piace alla comunità FLP) è esattamente ciò che voglio formalizzare con Coq! La mia fonte attuale è [un altro articolo] (http://homes.soic.indiana.edu/ccshan/rational/lazy-nondet.pdf) che modella esplicitamente una semantica simile al FLP del non-determinismo con le monadi. Dato che sto ancora cercando di capire quale modello sarebbe più adatto per essere usato in Coq, guarderò sicuramente la rappresentazione con le monade di Oleg "Freer" - per quanto mi ricordo, ho già letto carta (per un contesto diverso). Quindi grazie per il promemoria! – ichistmeinname

risposta

3

Vedere Chlipala's "Certified Programming with Dependent Types". Se avessi Definition Id T := T -> T, allora List Id potrebbe produrre un termine non terminante. Penso che potresti anche essere in grado di derivare una contraddizione dal Definition Not T := T -> False, specialmente se lasci il costruttore Nil e accetti la legge del mezzo escluso.

Sarebbe bello se ci fosse un modo per annotare M come solo utilizzando il suo argomento in posizioni positive. Penso che Andreas Abel abbia forse lavorato in questa direzione.

In ogni caso, se siete disposti a limitare le tipi di dato solo un po ', si potrebbe usare:

Fixpoint SizedList M A (n : nat) : Type := 
    match n with 
    | 0 => unit 
    | S m => option (M A * M (SizedList M A m)) 
    end. 

Definition List M A := { n : nat & SizedList M A n }. 
+1

Il lavoro di Abel in quella direzione è implementato in [MiniAgda] (http://www2.tcs.ifi.lmu.de/~abel/miniagda/). – gallais

+0

Grazie per la risposta rapida; sfortunatamente, ho dimenticato di scrivere che sono ancora un principiante in Coq. Potresti forse elaborare un po 'l'idea alla base di questa codifica? Ed è il modo giusto per definire i valori di tipo 'List M A' con' existT'? Questo tipo di costruzione è nuova per me e in qualche modo googling non ha aiutato. – ichistmeinname