與類型族匹配時的Coq類型錯誤

我試圖從內存中重新實現一個來自CPDT的示例。我寫道：與類型族匹配時的Coq類型錯誤

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.

產生的錯誤是：

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"

我不明白此錯誤消息。我認爲一旦Twice : unaryOp MyNat MyNat上的匹配成功，Coq推斷a和b是MyNat s，因此typeDenote a -> typeDenote b ≡ nat -> nat，使得twice成爲返回值的完美候選。我哪裏錯了？

來源

2016-07-15 Lynn

最後你的分析看起來非常好，所以我已經嘗試了一段代碼，但Coq完全沒有抱怨（使用Coq v8.4pl6和v8.5pl2進行檢查）。 –

就像@AntonTrunov說的，它在我的Coq 8.5pl1上沒有任何問題進行了類型檢查。但是，如果您需要爲您的版本添加一些額外的註釋以接受該功能，則您需要have a look at this section of the manual找出要執行的操作。

我的猜測是，你想有一個match ... in ... return ... with說，返回類型應該是精緻通過在類型unaryOp a b（事實上樹T獲得的信息：a和b將參加Twice分公司具體值）。

這是你開始使用該技術的定義：

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.

來源

2016-07-15 14:06:06 gallais

我認爲答案是Coq的類型推斷是有限的，並沒有做你想要的推理。

Coq的類型推斷不做任意的計算而是簡單的統一。它看起來在twice，明白它是nat->nat並得出結論，它不是typeDenote a -> TypeDenote b形式（語法上）。

如果它正在計算，它可能是非終止的，因爲它的類型系統非常複雜，所以你可以在那裏編碼非平凡的計算。

來源

2016-07-15 12:27:13 Elazar

我試過勒柯克的新版本，像其他人所說，這沒有問題typechecks上勒柯克8.5。 :)

來源

2016-07-15 16:41:29 Lynn

與類型族匹配時的Coq類型錯誤

回答

相關問題