CODEWITHSUNDEEP
functional-programmingagda
centrinok
centrinok

Reputation: 298

How to fix incomplete pattern matching in agda

Here's the code from a custom agda library. In the following code, 𝕍 stands for vector and β„• for Natural numbers. The take𝕍 type is similar to that of Haskell. Example: "take 3 [1,2,3,4,5,6,7,8]" results in [1,2,3]. 

take𝕍 : βˆ€{A : Set}{n : β„•} β†’ (m : β„•) β†’ 𝕍 A n β†’ 𝕍 A m
take𝕍 0 xs = []
take𝕍 (suc m) (x :: xs) = x :: take𝕍 m xs

I keep getting the error:

Incomplete pattern matching for take𝕍. Missing cases:
take𝕍 (suc m) [] when checking the definition of take𝕍

I dont understand, what possible proof I might be missing out.

Upvotes: 3

Views: 238

Answers (2)

effectfully
effectfully

Reputation: 12715

The type signature of take𝕍 says that for any completely unconstrained m you can return a Vec of length m having a Vec of length n. This is not true of course as m must be less or equal to n, because you want to return a prefix of a Vec. And since a number of elements to take and the length of a Vec are unrelated to each other, Agda gives you that error about incomplete pattern matching.

In Agda standard library the restriction that m is less or equal to the length of an input Vec is expressed as follows:

take : βˆ€ {a} {A : Set a} m {n} β†’ Vec A (m + n) β†’ Vec A m

You can also define something like

take : βˆ€ {a} {A : Set a} {m n} β†’ m ≀ n β†’ Vec A n β†’ Vec A m

Or even

take : βˆ€ {a} {A : Set a} m {n} β†’ Vec A n β†’ Vec A (m βŠ” n)

to model the behavior of Data.List.take (where _βŠ”_ means min in Agda stdlib).

Upvotes: 2

gallais
gallais

Reputation: 12093

You are pattern-matching on m and a vector xs of type 𝕍 A n. There is no guarantee that, because m is suc-headed that xs is non-empty. As the error suggests, you need to also consider the case where m is a suc and xs is empty.

Alternatively, you can write a function with a more precise type guaranteeing the fact that xs is at least as long as m. This is what is used in the standard library:

take : βˆ€ {A : Set} m {n} β†’ Vec A (m + n) β†’ Vec A m

Upvotes: 1

Related Questions