在伊德里斯

Question

恢復型

比方說，我有一個數據類型：

data Term : Type -> Type where 
    Id : Term (a -> a) 
    ... 
    App : Term (a -> b) -> Term a -> Term b 

有了一個證明事情是App：

data So : Bool -> Type where 
    Oh : So True 

isApp : Term a -> Bool 
isApp (App x y) = True 
isApp x   = False 

是否有可能編寫獲得的第一個參數的函數App？我不知道我怎麼會鍵入它，因爲原來的參數類型丟失：

getFn : (x : Term b) -> So (isApp x) -> ??? 
getFn (App f v) p = f 

我能保持Term以及指示什麼類型的已應用到它裏面的標籤，但後來我不得不將自己限制爲可標記類型。以前我會認爲這是唯一的選擇，但在我認爲我會先問的依賴類型的土地上似乎會發生這麼多神奇的事情。

（阿格達例子是值得歡迎的好，雖然我更喜歡那些伊德里斯！）

Answer 1

肯定。我沒有這臺機器上的伊德里斯編譯器，但這裏是在阿格達的解決方案：

open import Data.Bool.Base 

data Term : Set -> Set₁ where 
    Id : ∀ {a} -> Term (a -> a) 
    App : ∀ {a b} -> Term (a -> b) -> Term a -> Term b 

data So : Bool -> Set where 
    Oh : So true 

isApp : ∀ {a} -> Term a -> Bool 
isApp (App x y) = true 
isApp x   = false 

GetFn : ∀ {b} -> (x : Term b) -> So (isApp x) -> Set₁ 
GetFn Id    () 
GetFn (App {a} {b} f x) _ = Term (a -> b) 

getFn : ∀ {b} -> (x : Term b) -> (p : So (isApp x)) -> GetFn x p 
getFn Id  () 
getFn (App f v) p = f 

你只需要在類型和值水平，以明確放棄Id案件。然後GetFn (App f x)返回所需的類型，然後getFn (App f x)返回所需的值。

這裏的關鍵部分是，當你寫getFn (App f v)x獲取與App f v統一，類型簽名變得GetFn (App f v) p，這簡化了Term (a -> b)爲適當a和b，這也正是f類型。

或者你可以寫

GetFn : ∀ {b} -> Term b -> Set₁ 
GetFn Id    = junk where junk = Set 
GetFn (App {a} {b} f x) = Term (a -> b) 

getFn : ∀ {b} -> (x : Term b) -> So (isApp x) -> GetFn x 
getFn Id  () 
getFn (App f v) p = f 

getFn丟棄Id，所以我們不關心的垃圾是GetFn回報在Id情況。

編輯

我想在伊德里斯你需要在App構造了a和b明確量化。