圖案上的類型的計算功能在伊德里斯結果

Question

考慮以下片段匹配：

import Data.List 

%default total 

x : Elem 1 [1, 2] 
x = Here 

type : Type 
type = Elem 1 [1, 2] 

y : type 
y = Here 

這給出了錯誤：

當檢查Y的右側：之間 ELEM X 類型不匹配（X :: XS）（這裏的類型） 和 ITYPE（預期類型）

類型的y，在查詢時，是：

type : Type 
----------- 
y : type 

是否有可能迫使type期間或y類型歸屬之前進行評估，從而使y類型是Elem 1 [1, 2]？

我使用的情況是，我希望能夠定義返回正確的命題條款證明通用謂詞，例如：

subset : List a -> List a -> Type 
subset xs ys = (e : a) -> Elem e xs -> Elem e ys 

thm_filter_subset : subset (filter p xs) xs 

Answer 1

名稱在類型聲明與小寫字母開頭是含蓄所以它將'type'視爲一個類型參數。你可以給'type'一個以大寫字母開頭的新名字（按照慣例，這是大多數人在Idris中做的），或者你可以明確地使用它所在的模塊（Main，here）來限定名字。

Idris用於嘗試猜測名稱（如'type'）是作爲隱式還是意圖指向全局，如此處所示。儘管如此，所有這些都涉及到巫術，所以它經常失敗，所以它現在實現了這個更簡單的規則。在這種情況下，這有些惱人，但另一種行爲往往更令人討厭（而且更難以解釋）。