在agda中依賴類型的捲曲

我認爲你可以在Agda中任意功能。這樣您就可以隨時調換輸入的順序。在agda中依賴類型的捲曲

，並表示，即使編譯一個定理：

curry : {A : Set} -> {B : Set} -> {C : Set} -> (A -> B -> C) -> (B -> A -> C) 
curry f b a = f a b

然而，阿格達具有依賴型和類似

curry' : {A : Set} -> {B : (A -> Set) } -> { C : (A -> Set) } -> ((a : A) -> B a -> C a) -> (B a -> (a : A) -> C a)

甚至不進行編譯。

由於(a : A) -> B a -> C a與A -> B -> C一樣有效我開始覺得你不能一般咖喱。儘管在a : A之前遞交函數B a似乎沒什麼特別可怕的。

有沒有一些一般的執行咖喱的技巧？或者Agda不可能？

來源

2014-06-22 user833970

你所描述的不是捲曲。這是一個簡單的參數交換。

這裏的鑽營的樣子：

open import Data.Product 
    hiding (curry) 

-- non-dependent version 
curry′ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} → 
     (A × B → C) → (A → B → C) 
curry′ f a b = f (a , b) 

-- dependent version 
curry : ∀ {a b c} {A : Set a} {B : A → Set b} {C : Set c} → 
     (Σ A B → C) → ((a : A) → B a → C) 
curry f a b = f (a , b)

C可能還取決於A和B;完全依賴版本可以在Data.Product中找到。

總而言之，這是除了點。您想要的操作（即depenent swap）無法在Agda中執行 - 也適用於大多數其他依賴型理論。

來源

2014-06-22 03:11:31 Vitus

，如果你使用這兩個功能相同a : A可以把它定義，即

foo : {A : Set} {B C : A → Set}(a : A) → 
     (A → B a → C a) → 
     (B a → A → C a) 
foo a f Ba _ = f a Ba

來源

2014-06-22 03:40:03 asr

你可以做這樣的事情：

open import Level 
open import Function hiding (id) 
open import Data.Nat 
open import Data.Vec 

data Id {α : Level} {A : Set α} : A -> Set α where 
    id : (x : A) -> Id x 

flip-id : {α β γ : Level} {A : Set α} {B : A -> Set β} {C : (x : A) -> B x -> Set γ} {x : A} 
     -> ((x : A) -> (y : B x) -> C x y) -> (y : B x) -> Id x -> C x y 
flip-id f y (id x) = f x y 

test-func : (n : ℕ) -> Vec ℕ n -> ℕ 
test-func n _ = n 

{-error : ℕ 
error = flip test-func (0 ∷ 0 ∷ []) 2-} 

ok : ℕ 
ok = flip-id test-func (0 ∷ 0 ∷ []) (id 2)

還有對稱函數：

id-flip : {α β γ : Level} {A : Set α} {B : A -> Set β} {C : (x : A) -> B x -> Set γ} 
     -> ({x : A} -> (y : B x) -> Id x -> C x y) -> (x : A) -> (y : B x) -> C x y 
id-flip f x y = f y (id x)

來源

2014-06-22 13:30:33 user3237465

在agda中依賴類型的捲曲

回答

相關問題