All geek questions in one place

How to use dependent pairs

Suppose I have a function (it really does what the name says):

filter : βˆ€ {A n} β†’ (A β†’ Bool) β†’ Vec A n β†’ βˆƒ (Ξ» m β†’ Vec A m)

Now I would like to somehow work with the dependent pair that I am returning. I wrote a simple head function:

 head :: βˆ€ {A} β†’ βˆƒ (Ξ» n β†’ Vec A n) β†’ Maybe A head (zero , _ ) = nothing head (succ _ , (x :: _)) = just x

which of course works great. But it made me wonder: is there a way I can make sure that a function can only be called with n β‰₯ 1 ?

Ideally, I would like to make a head : βˆ€ {A} β†’ βˆƒ (Ξ» n β†’ Vec A n) β†’ IsTrue (n β‰₯ succ zero) β†’ A function head : βˆ€ {A} β†’ βˆƒ (Ξ» n β†’ Vec A n) β†’ IsTrue (n β‰₯ succ zero) β†’ A ; but this fails because n goes out of scope when I use it in IsTrue .

Thank you for your time!

IsTrue looks something like this:

 data IsTrue : Bool β†’ Set where check : IsTrue true
+4
source share
4 answers

I think this is a question of dispassion. The standard library provides unmanaged functions for products, see uncurry . It would be more beneficial for your situation to have a non-alienation function where the first argument is hidden, since the head function usually takes a length index as an implicit argument. We can write a fatal function such as:

 uncurryΚ° : βˆ€ {abc} {A : Set a} {B : A β†’ Set b} {C : (a : A) β†’ B a β†’ Set c} β†’ ({x : A} β†’ (y : B x) β†’ C xy) β†’ ((p : Ξ£ AB) β†’ uncurry C p) uncurryΚ° f (x , y) = f {x} y

The function that returns the head of the vector, if there is one, does not seem to exist in the standard library, so we write one:

 maybe-head : βˆ€ {an} {A : Set a} β†’ Vec A n β†’ Maybe A maybe-head [] = nothing maybe-head (x ∷ xs) = just x

Now your desired function is just a possibly-head question with the first-argument-implicit-unmanaged function defined above:

 maybe-filter-head : βˆ€ {A : Set} {n} β†’ (A β†’ Bool) β†’ Vec A n β†’ Maybe A maybe-filter-head p = uncurryΚ° maybe-head ∘ filter p

Conclusion: dependent products look happy and ugly, as do their independent versions.

Leaving aside, the function you want to write with a signature like

 head : βˆ€ {A} β†’ βˆƒ (Ξ» n β†’ Vec A n) β†’ IsTrue (n β‰₯ succ zero) β†’ A

It can be written as:

 head : βˆ€ {A} β†’ (p : βˆƒ (Ξ» n β†’ Vec A n)) β†’ IsTrue (proj₁ p β‰₯ succ zero) β†’ A
+3
source

After playing with him for some time, I came up with a solution similar to the function that I wanted in the first place:

 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

If someone comes up with a better (or more general) solution, I will gladly accept their answer. Comments are also welcome.

Here I came up with a more general predicate:

 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 ...
+1
source

The best way is probably to break the dependent pair first so you can simply write:

 head :: βˆ€ {A n} β†’ Vec A (S n) β†’ A

However, if you really want the dependent pair to be intact in the function signature, you can write the PosN predicate, which checks the first element of the pair and checks that it is positive:

 head :: βˆ€ {A p} β†’ PosN p -> A

or similar. I will leave the definition of PosN as an exercise for the reader. Essentially, this is what Vitas's answer already does, but instead a simpler predicate can be defined.

+1
source

This is like a regular head function for Vec .

 head' : βˆ€ {Ξ±} {A : Set Ξ±} β†’ βˆƒ (Ξ» n β†’ Vec A (suc n)) β†’ A head' (_ , x ∷ _) = x
0
source

Source: https://habr.com/ru/post/1400476/

More articles:


All Articles