đối số chiều dài Tiềm ẩn trong chiều dài cố định-vector-chức năng trong Agda

Question

tôi đã viết một Agda chức năng prefixApp áp dụng một Vector-Function để một tiền tố của một vector:

split : {A : Set}{m n : Nat} -> Vec A (n + m) -> (Vec A n) * (Vec A m) 
split {_} {_} {zero} xs  = ([] , xs) 
split {_} {_} {suc _} (x :: xs) with split xs 
... | (ys , zs) = ((x :: ys) , zs) 

prefixApp : {A : Set}{n m k : Nat} -> (Vec A n -> Vec A m) -> Vec A (n + k) -> Vec A (m + k) 
prefixApp f xs with split xs 
... | (ys , zs) = f ys ++ zs 

Tôi thích thực tế, rằng prefixApp có thể được sử dụng mà không cung cấp một đối số chiều dài một cách rõ ràng, ví dụ

gate : Vec Bool 4 -> Vec Bool 3 
gate = prefixApp xorV 

(nơi xorV : Vec Bool 2 -> Vec Bool 1 là Vector-XOR-Function)

Thật không may, tôi không biết làm thế nào để viết một postfixApp -function mà có thể được sử dụng mà không cung cấp một cách rõ ràng một cuộc tranh luận dài. định nghĩa hàm của tôi cho đến nay trông như thế này:

postfixApp : {A : Set}{n m k : Nat} -> (Vec A n -> Vec A m) -> Vec A (k + n) -> Vec A (k + m) 
postfixApp {_} {_} {_} {k} f xs with split {_} {_} {k} xs 
... | (ys , zs) = ys ++ (f zs) 

Dường như, tuy nhiên, postfixApp luôn cần một cuộc tranh luận dài. Ví dụ.

gate : Vec Bool 4 -> Vec Bool 3 
gate = postfixApp {k = 2} xorV 

Có ai biết, làm thế nào để loại bỏ đối xứng này, ví dụ: làm thế nào để viết một hàm postfixApp mà hoạt động mà không một cuộc tranh cãi dài rõ ràng. Tôi đoán, tôi cần một số khác split-chức năng?

Answer 1

Với prefixApp của bạn, bạn có

prefixApp : {A : Set}{n m k : Nat} -> (Vec A n -> Vec A m) -> Vec A (n + k) -> Vec A (m + k) 

và bạn vượt qua nó một chức năng Vec Bool 2 -> Vec Bool 1, vì vậy nó biết rằng n = 2 và m = 1 bởi thống nhất đơn giản. Sau đó, vì phép cộng được xác định bằng đệ quy trên các đối số bên trái, phần còn lại của loại hàm giảm từ Vec A (2 + k) -> Vec A (1 + k) xuống Vec A (suc (suc k)) -> Vec A (suc k). Sau đó, Agda có thể áp dụng hợp nhất thẳng hàng (mở rộng số lượng chữ) của:

Vec A (suc (suc k)) -> Vec A (suc k) 
Vec Bool (suc (suc (suc (suc zero)))) -> Vec Bool (suc (suc (suc zero))) 

để suy ra rằng k = 2.

Nhìn vào một trong những khác:

postfixApp : {A : Set}{n m k : Nat} -> (Vec A n -> Vec A m) -> Vec A (k + n) -> Vec A (k + m) 

Sự khác biệt duy nhất là số lượng biết rằng xorV bạn lực lượng n và m là 2 và 1, nhưng điều này chỉ làm cho phần còn lại của loại chức năng của bạn vào Vec A (k + 2) -> Vec A (k + 1) . Loại này không giảm hơn nữa, bởi vì phần bổ sung được xác định bằng cách đệ quy trên đối số đầu tiên, k, không xác định tại thời điểm này. Sau đó, bạn cố gắng hợp nhất k + 2 với 4 và k + 1 với 3 và Agda phun ra màu vàng. "Nhưng rõ ràng là k = 2", bạn nói! Bạn biết rằng bởi vì bạn biết toán học, và có thể áp dụng phép trừ và các nguyên tắc đơn giản khác, nhưng Agda không biết điều đó. _+_ chỉ là một chức năng khác, và việc hợp nhất các ứng dụng chức năng tùy ý là khó. Nếu tôi yêu cầu bạn hợp nhất (2 + x) * (2 + y) với 697, chẳng hạn? Liệu người đánh máy có được dự kiến ​​là nhân tố số và phàn nàn rằng không có một yếu tố duy nhất? Tôi đoán kể từ khi nhân là giao hoán thường sẽ không được trừ khi bạn hạn chế các bên, nhưng nên Agda biết rằng phép nhân là giao hoán?

Dù sao đi nữa, vì vậy Agda chỉ biết cách hợp nhất, về cơ bản khớp với số lượng "kết cấu" với nhau.Các nhà xây dựng dữ liệu có chất lượng cấu trúc này đối với họ, cũng như các nhà xây dựng kiểu, vì vậy tất cả các nhà xây dựng có thể được thống nhất một cách rõ ràng. Khi nói đến bất cứ điều gì huyền ảo hơn thế, bạn gặp phải vấn đề "thống nhất trật tự cao hơn", mà không thể giải quyết được. Agda thực hiện một thuật toán ưa thích được gọi là thống nhất mẫu Miller, cho phép nó giải quyết một số tình huống hạn chế về tình huống, nhưng có một số thứ mà nó không thể làm được, và loại ứng dụng chức năng của bạn là một trong số chúng.

Nếu bạn nhìn vào thư viện chuẩn, bạn sẽ thấy rằng hầu hết các trường hợp liên quan đến việc bổ sung naturals, một trong các phần bổ sung (phần bên trái) thường không bị ẩn, trừ khi một đối số khác chỉ định nó hoàn toàn (như trường hợp trong số prefixApp) của bạn.

Theo như những gì cần làm về nó, không có nhiều để giải quyết vấn đề nói chung. Sau một thời gian, bạn phát triển một ý nghĩa cho những gì Agda có thể suy luận và những gì nó không thể, và sau đó ngừng làm cho các đối số không thể chấp nhận ngầm. Bạn có thể xác định một phiên bản "đối xứng" của _+_, nhưng nó kết thúc lên chỉ là đau đớn không kém để làm việc với cả hai mặt của nó, vì vậy tôi không khuyên bạn nên.

Answer 2

Thực tế, có thể xác định hàm này với cùng loại.

postfixApp : {A : Set}{n m k : ℕ} -> (Vec A n -> Vec A m) -> Vec A (n + k) -> Vec A (k + m) 
postfixApp f xs with splitAt' (reverse xs) 
... | ys , zs = reverse zs ++ f (reverse ys) 

test-func : Vec Bool 3 -> Vec Bool 2 
test-func (x1 ∷ x2 ∷ x3 ∷ []) = (x1 ∧ x2) ∷ (x2 ∨ x3) ∷ [] 

test : postfixApp test-func (false ∷ false ∷ true ∷ false ∷ true ∷ []) 
          ≡ false ∷ false ∷ false ∷ true ∷ [] 
test = refl 

Toàn bộ mã: http://lpaste.net/107176