filter for vector, a question

[Falko]

Hello,

probably I get somewhat demanding, but if anybody has the time to explain in simple words, why filter1 (a copy from prelude) works, and
filter2 doesn't?
How can p be understood by the type checker in one case, and not in the other?

> total filter1 : (a -> Bool) -> Vect a n -> (p ** Vect a p)
> filter1 p [] = ( _ ** [] )
> filter1 p (x::xs) with (filter1 p xs)
>   | (_ ** tail) =
>     if p x then
>       (_ ** x::tail)
>     else
>       (_ ** tail)

> filter2 : (a -> Bool) -> Vect a n -> Vect a p
> filter2 p [] = []
> filter2 p (x::xs) with (filter2 p xs)
>   | tail =
>     if p x then
>       x::tail
>     else
>       tail

Is there a way to make filter2 work?

Thank you, and greetings, Falko

[Daniel Peebles]

They're fundamentally different types. In `filter1`, `p` is existential. It says "you can give me a predicate, a vector of a length of your choice, and I'll give you a vector of some length that I choose"

The type of `filter2` says "you give me a predicate, a vector of a length of your choice, and I'll give you a vector of another length of your choice".

You might envision writing some weird behavior, for example, if `p` is smaller than `n`, you could truncate the result. If it's longer than `n`, you could repeat the last element up until `p`. The only problem with that signature is what to do if `n` is 0 and `p` is not (and the predicate doesn't reject all elements). Then you need to produce elements of type `a` from nowhere, which is impossible, so that function can't be written in a total manner. If you could, you could easily prove false by providing `const True` as your predicate, the empty type for `a`, 0 for `n`, and 1 for `p`. Then just take the head of the resulting `Vec _|_ 1` and you have your proof of false :)

 Does that help at all?

[Daniel Peebles]

Just to elaborate a tiny bit, what I mean is that not only is it not possible to write (a function with the same type as) `filter2`, but we can actually prove that it is impossible, in Idris.

On Wed, Nov 28, 2012 at 3:37 PM, Falko <falko....@gmail.com> wrote:

[raichoo]

Here is my naive take on it (and please correct me when I'm wrong).

Let's look at the type of filter

 filter2 : (a -> Bool) -> Vect a n -> Vect a p

and expand it a little bit. We know that p is of type Nat

therefore we the type could be expanded to:

 filter2 : {p : Nat} -> (a -> Bool) -> Vect a n -> Vect a p

From a logic perspective this means. Forall p I can take

a predicate and a vector of length n and produce a vector

of length p.

This is not what filter should do at all.

We know that after filtering the vector we there

should exist a vector of some lenght p.

Therefore the type has to be

 filter : (a -> Bool) -> Vector a n -> (p ** Vect a p)

Kind regards

raichoo

[raichoo]

Please excuse the numerous typos. Whenever reformulating a sentence I tend to mess up :/

[Falko]

Hello Daniel, hello raichoo,

fascinating. I still did not know about existential types at all. How should I have recognized that?

So. Hm. Can I make p in filter2 existential? (If I understand Daniel right, I somehow have to tell p < n, do I?)

The point is, I want a vector, not a pair containing a vector.

Thank you very much for the explanations,

Falko

[Falko]

@raichoo ;-))

[raichoo]

You can have your cake and eat it :)

Idris> let x : (n ** Vect Int n) = (_ ** [1,2,3]) in getProof x

Prelude.Vect.:: 1 (Prelude.Vect.:: 2 (Prelude.Vect.:: 3 (Prelude.Vect.Nil))) : Vect Int (S (S (S O)))

Kind regards,

raichoo

[Daniel Peebles]

The big realization is that the pair is the existential :) Having a pair of a natural `p` and a vector of length `p` is the same as just saying "a vector of some length". This is but one of the powers of Sigma! :)

So in that sense, to make `filter2` existential, you give it the same type (and definition, probably) as `filter1` :)

Your idea would also work (using <=, not <), but the `p` in `filter2` would still be universal. It would just be constrained a bit more to make sense. So you should be able to write:

filter2 : p <= n -> (a -> Bool) -> Vect a n -> Vect a p

But it'll have to do ugly things like what I described in my earlier email (which makes it kind of odd to call it filter). That is, you'd have to effectively run `filter1`, then take its result and either truncate it or extend it to be of length `p`.

[Falko]

I just try to think in that direction. But what type would this have?

filter2 p v = getProof $ filter1 p v

Hm.

:t (\p,x => getProof $ filter1 p x)
INTERNAL ERROR: "Nothing to introduce"
This is probably a bug, or a missing error message.
Please consider reporting at https://github.com/edwinb/Idris-dev/issues

;-)

Nice evening, f.

[raichoo]

The problem with "wanting a vector" is that you have to know the type.

You can think of types as sets.

Vect is an inductive family which means that you can think if it as

a family of sets indexed by the natural numbers.

Now to know which member of the family we mean, we need a

witness, that's the first component of the dependent pair.

The other component is the proof and it's term depends on the

value of the witness.

These pairs are called Sigma types or dependent pairs and

they generalize the pairs you know from languages like haskell etc.

Kind regards,

raichoo

[Falko]

@reichoo

I understand (or so I think). But where do I see that p in filter1 is, in Daniels words, "some length that I (the program) choose", and in filter2 a "length of your (programmers) choice".

Is there something hidden in the ( .. ** ..) syntax that I'm not aware of?

Well, I'll go on reading tomorrow.

Bye for today, Falko

[Arthur Peters]

I didn't know the syntax used for dependent pairs in Idris. So I did a quick search for it and I found this:

http://www.cs.st-andrews.ac.uk/~eb/Idris/stdlib.html

I figure it might help. The point is that the dependent pair is just a type declared in the language. It's not a built-in type in any way. So yes, there is something hidden but it's just the type definition. Which is given nicely on that page (which BTW I have no idea if it works on modern Idris, it might be for an old version).

-Arthur

[Edwin Brady]

On 28 Nov 2012, at 21:54, Arthur Peters <a...@singingwizard.org> wrote:

> I didn't know the syntax used for dependent pairs in Idris. So I did a quick search for it and I found this:
>
> http://www.cs.st-andrews.ac.uk/~eb/Idris/stdlib.html

Hmm, I should put a redirect on that - it refers to the old (0.1.n) version.

Edwin.

[Arthur Peters]

Perhaps but to me (not very experiences with any of this) it's actually a fairly good quick intro to dependent pairs and how they are defined in a language like Idris. So the content seems worth keeping.

-Arthur

[raichoo]

Daniel gave a nice introduction to Agda in which he explains the

concepts of Sigma and Pi types. I think it's a good primer when you

want to adjust your thinking to dependent types (they can be pretty

mind bending :)

http://www.youtube.com/watch?v=shXKb2MTkUc

I can really recommend watching this (it helped me, that's for sure :)

Kind regards,

raichoo