Coq-Typ Fehler beim Abgleich mit Typ Familie

Question

Ich versuche, ein Beispiel aus CPDT aus dem Speicher zu re-implementieren. Ich schrieb:

Inductive myType : Set := MyNat | MyBool. 

Definition typeDenote (t : myType) : Set := 
    match t with 
    | MyNat => nat 
    | MyBool => bool 
    end. 

Inductive unaryOp : myType -> myType -> Set := 
| Twice : unaryOp MyNat MyNat. 

Definition twice (n:nat) : nat := n + n. 

Definition tunaryDenote (a b : myType) (t : unaryOp a b) 
    : typeDenote a -> typeDenote b := 
    match t with 
    | Twice => twice 
    end. 

Der resultierende Fehler ist:

Toplevel input, characters 125-130 
> | Twice => twice 
>    ^^^^^ 
Error: In environment 
a : myType 
b : myType 
t : unaryOp a b 
The term "twice" has type "nat -> nat" while it is expected to have type 
"forall H : typeDenote ?141, typeDenote ?142" 

Ich verstehe nicht, diese Fehlermeldung. Ich würde denken, dass, sobald das Spiel auf Twice : unaryOp MyNat MyNat erfolgreich ist, Coq schließt, dass a und b sind MyNat s, und damit typeDenote a -> typeDenote b ≡ nat -> nat, machen twice eine perfekte Kandidat für den Rückgabewert. Wo bin ich falsch gelaufen?

Answer 1

Genau wie @AntonTrunov sagte, es ist ohne Problem auf meinem Coq 8.5pl1 typchecked. Wenn Sie jedoch zusätzliche Anmerkungen für Ihre Version hinzufügen müssen, um die Funktion zu akzeptieren, müssen Sie have a look at this section of the manual herausfinden, was zu tun ist.

Mein guess IS dass Sie Mangel zu have ein match ... in ... return ... with zu say dass die return type Should seist refined durch die Informationen obtained durch matching t am type unaryOp a b (indeed: a und b Wille take concrete values ​​im Twice branch).

Dies ist die Definition Sie diese Technik erhalten werden:

Definition tunaryDenote (a b : myType) (t : unaryOp a b) 
    : typeDenote a -> typeDenote b := 
    match t in unaryOp a b return typeDenote a -> typeDenote b with 
    | Twice => twice 
    end. 

Answer 2

Ich denke, dass die Antwort ist, dass Coqs Typ Rückschluss begrenzt ist, und nicht die Argumentation tun, die Sie es tun möchten.

Coq-Typ-Inferenz führt keine willkürlichen Berechnungen, sondern einfache Vereinheitlichung durch. Es sieht twice, verstehen, dass es nat->nat ist und schließt daraus, dass es nicht (syntaktisch) der Form typeDenote a -> TypeDenote b ist.

Wenn es Berechnungen durchführte, war es wahrscheinlich, dass es nicht beendet wurde, da sein Typsystem sehr hoch entwickelt ist, so dass Sie dort nicht-triviale Berechnungen codieren können.

Answer 3

ich eine neuere Version von Coq versucht, und wie andere gesagt haben, typechecks es ohne Problem auf Coq 8.5. :)