كيفية استخدام الأزواج التابعة

Question

لنفترض أن لدي وظيفة (وهي في الواقع تفعل ما يقوله الاسم):

filter : ∀ {A n} → (A → Bool) → Vec A n → ∃ (λ m → Vec A m)

الآن، أود العمل بطريقة ما مع الزوج التابع الذي أعود إليه.لقد كتبت بسيطة head وظيفة:

head :: ∀ {A} → ∃ (λ n → Vec A n) → Maybe A
head (zero   , _ )       = nothing
head (succ _ , (x :: _)) = just x

والذي يعمل بالطبع على أكمل وجه.لكنه جعلني أتساءل:هل هناك أي طريقة يمكنني من خلالها التأكد من أنه لا يمكن استدعاء الوظيفة إلا باستخدام n ≥ 1?

من الناحية المثالية، أود أن أجعل الوظيفة head : ∀ {A} → ∃ (λ n → Vec A n) → IsTrue (n ≥ succ zero) → A;ولكن هذا فشل، لأن n خارج النطاق عندما أستخدمه IsTrue.

شكرا على وقتك!

---

IsTrue شيء مثل:

data IsTrue : Bool → Set where
  check : IsTrue true

Answer 1

أعتقد أن هذا سؤال حول عدم الاهتمام.توفر المكتبة القياسية وظائف غير متوفرة للمنتجات ، انظر غير متوقع.بالنسبة لموقفك ، سيكون من المفيد أن يكون لديك وظيفة غير متوفرة حيث يتم إخفاء الوسيطة الأولى ، لأن وظيفة الرأس عادة ما تأخذ فهرس الطول كوسيطة ضمنية.يمكننا كتابة دالة غير منتظمة مثل هذا:

uncurryʰ : ∀ {a b c} {A : Set a} {B : A → Set b} {C : (a : A) → B a → Set c} →
           ({x : A} → (y : B x) → C x y) →
           ((p : Σ A B) → uncurry C p)
uncurryʰ f (x , y) = f {x} y

الوظيفة التي تُرجع رأس المتجه إذا كان هناك واحد لا يبدو أنه موجود في المكتبة القياسية ، لذلك نكتب واحدة:

maybe-head : ∀ {a n} {A : Set a} → Vec A n → Maybe A
maybe-head []       = nothing
maybe-head (x ∷ xs) = just x

الآن ، فإن الوظيفة المطلوبة هي مجرد مسألة رفع وظيفة الرؤوس من خلال الوظيفة الأولى التي تتمثل في الإلغاء المحددة أعلاه:

maybe-filter-head : ∀ {A : Set} {n} → (A → Bool) → Vec A n → Maybe A
maybe-filter-head p = uncurryʰ maybe-head ∘ filter p

خاتمة:المنتجات التابعة الكاري بكل سرور وغير الكاري مثل الإصدارات غير التابعة لها.

بغض النظر عن الوظيفة التي تريد كتابتها بتوقيع النوع

head : ∀ {A} → ∃ (λ n → Vec A n) → IsTrue (n ≥ succ zero) → A

يمكن كتابتها على النحو التالي:

head : ∀ {A} → (p : ∃ (λ n → Vec A n)) → IsTrue (proj₁ p ≥ succ zero) → A

Answer 2

أفضل طريقة هي على الأرجح تدمير الزوج التابع أولًا، بحيث يمكنك فقط كتابة:

head :: ∀ {A n} → Vec A (S n) → A

ومع ذلك، إذا كنت تريد حقًا الحفاظ على الزوج التابع سليمًا في توقيع الدالة، فيمكنك كتابة PosN المسند الذي يتفقد العنصر الأول من الزوج ويتحقق من أنه موجب:

head :: ∀ {A p} → PosN p -> A

أو مشابه.سأترك تعريف PosN كتمرين للقارئ.هذا هو ما تفعله إجابة فيتوس بالفعل، ولكن يمكن تعريف مسند أبسط بدلاً من ذلك.

Answer 3

بعد اللعب بها لبعض الوقت، توصلت إلى حل يشبه الوظيفة التي أردتها في المقام الأول:

data ∃-non-empty (A : Set) : ∃ (λ n → Vec A n) → Set where
  ∃-non-empty-intro : ∀ {n} → {x : Vec A (succ n)} → ∃-non-empty A (succ n , x)

head : ∀ {A} → (e : ∃ (λ n → Vec A n)) → ∃-non-empty A e → A
head (zero   , [])       ()
head (succ _ , (x :: _)) ∃-non-empty-intro = x

إذا توصل أي شخص إلى حل أفضل (أو أكثر عمومية)، فسأقبل إجابته بكل سرور.التعليقات هي موضع ترحيب أيضا.

---

إليك المسند الأكثر عمومية الذي توصلت إليه:

data ∃-succ {A : Nat → Set} : ∃ A → Set where
  ∃-succ-intro : ∀ {n} → {x : A (succ n)} → ∃-succ (succ n , x)

-- or equivalently
data ∃-succ {A : Nat → Set} : ∃ (λ n → A n) → Set where
  ...

Answer 4

هذا هو تماما مثل المعتاد head وظيفة ل Vec.

head' : ∀ {α} {A : Set α} → ∃ (λ n → Vec A (suc n)) → A
head' (_ , x ∷ _) = x