Request for comments on the elemList exercise

[Chetan Taralekar]

I'm following the videos from the workshop that Edwin Brady is giving. 

In the first video (https://vimeo.com/61576198 around 1:10:10 mark), Edwin mentions a more correct version of elemList , one that returns Dec (Elem x xs).

Below is a solution (it typechecks with the latest version).

Since I'm just beginning to learn dependently typed programming (mostly on Coq), I wanted people's opinions on the version below.

Any comments on how it could be better/shorter/cleaner are welcome.

Some stuff I noticed, 

1. Removing the second case in elemNilContra (the "There" branch) did not make isElem2 non-total. Is that expected, or an issue with the totality checker?

2. In the beginning, I actually put the following definition of elemNilContra, and it typechecked. This obviously is a bug?

     elemNilContra : (x : Nat) -> (Elem x (Prelude.List.Nil)) -> _|_

     elemNilContra refl impossible

-------------------------- CODE FOLLOWS

module Test

import Decidable.Equality

using (xs : List a)

  data Elem : a -> List a -> Type where

       Here  : Elem x (x :: xs)

       There : Elem x xs -> Elem x (y :: xs)

total

isElem : (x : Nat) -> (xs : List Nat) -> Maybe (Elem x xs)

isElem x [] = Nothing

isElem x (y :: ys) with (decEq x y)

  isElem x (x :: ys) | Yes refl = [| Here |]

  isElem x (y :: ys) | No  _    = [| There (isElem x ys) |]

elemListContra : (x : Nat) -> (y : Nat) -> ((x = y) -> _|_) -> (ys : List Nat) -> ((Elem x ys) -> _|_) -> (Elem x (y :: ys)) -> _|_

elemListContra _ _ x_ne_y _ x_ni_ys Here       = x_ne_y  refl

elemListContra _ _ x_ne_y _ x_ni_ys (There e') = x_ni_ys e'

elemNilContra : (x : Nat) -> (Elem x (Prelude.List.Nil)) -> _|_

elemNilContra x Here impossible

elemNilContra x (There _) impossible

total

isElem2 : (x : Nat) -> (xs : List Nat) -> Dec (Elem x xs)

isElem2 x [] = No (elemNilContra x)

isElem2 x (y :: ys) with (decEq x y)

  isElem2 x (x :: ys) | Yes refl = Yes Here

  isElem2 x (y :: ys) | No  no   = case isElem2 x ys of

                                     Yes yep => Yes (There yep)

                                     No nope => No (elemListContra x y no ys nope)

[David Christiansen]

Hi Chetan,

> I'm following the videos from the workshop that Edwin Brady is giving.

Welcome to the Idris list! I'm glad to see that the videos are
spreading, so it's not just us lucky ITU students who can get the
benefit of Edwin's course!

> In the first video (https://vimeo.com/61576198 around 1:10:10 mark), Edwin
> mentions a more correct version of elemList , one that returns Dec (Elem x
> xs).
>
> Below is a solution (it typechecks with the latest version).
> Since I'm just beginning to learn dependently typed programming (mostly on
> Coq), I wanted people's opinions on the version below.
>
> Any comments on how it could be better/shorter/cleaner are welcome.

Your code looks quite good to me. I would probably lay out some of the
longer type signatures a bit differently to make them a bit more
readable, especially in elemListContra, but this is a very minor
thing. I'd probably also write the type of elemNilContra as follows:

elemNilContra : (x : Nat) -> (Elem x []) -> _|_

The [] disambiguates fine for me, anyway.

> Some stuff I noticed,
> 1. Removing the second case in elemNilContra (the "There" branch) did not
> make isElem2 non-total. Is that expected, or an issue with the totality
> checker?

The totality checker has some issues :-) If you keep following the
lectures, you'll hear Edwin point out that it's best used as an extra
safety net rather than as something that you base all of your
soundness on. It does seem to be improving though!

On the other hand, it could be the case that the totality checker is
smarter than we think - it won't typecheck a single-case definition

elemNilContra x prf impossible

but it may be the case that a single impossible declaration is enough
for the type and totality checkers to see that the There branch can
never be type-correct, and therefore be total. In general, impossible
is just necessary to convince the totality checker that some
particular impossible case can't happen - it will eliminate many of
them on its own. I'm not familiar enough with that part of the
implementation to tell for sure what's happening.

> 2. In the beginning, I actually put the following definition of
> elemNilContra, and it typechecked. This obviously is a bug?
> elemNilContra : (x : Nat) -> (Elem x (Prelude.List.Nil)) -> _|_
> elemNilContra refl impossible

I would certainly see the acceptance of your first elemNilContra as a
bug! 'refl' clearly can't be a pattern for Nat. You can open a ticket
at https://github.com/edwinb/Idris-dev/issues .

/David

[Edwin Brady]

On 18 Mar 2013, at 10:25, David Christiansen <da...@davidchristiansen.dk> wrote:

>> 2. In the beginning, I actually put the following definition of
>> elemNilContra, and it typechecked. This obviously is a bug?
>> elemNilContra : (x : Nat) -> (Elem x (Prelude.List.Nil)) -> _|_
>> elemNilContra refl impossible
>
> I would certainly see the acceptance of your first elemNilContra as a
> bug! 'refl' clearly can't be a pattern for Nat. You can open a ticket
> at https://github.com/edwinb/Idris-dev/issues .

elemNilControl refl is certainly impossible. The 'impossible' keyword just verifies that the pattern doesn't type check.

Edwin.

[David Christiansen]

> elemNilControl refl is certainly impossible. The 'impossible' keyword just verifies that the pattern doesn't type check.

Hi Edwin,

I suppose that this makes sense :-) However, it does seem to be
somehow "more impossible" than the actual, desired definition -
perhaps it might make sense to warn if the pattern creates a
completely different type, rather than the same constructor but with
different indices / parameters?

(I realize I'm in "damn user wishlist without a patch" territory,
which is even worse than bikeshedding, but still...)

/David

[Chetan Taralekar]

I can understand elemNilControl refl being impossible.

But I can't understand why having just that case would pass typechecking, since there isn't any other case(Here/There) covered. 

Is that intended?

[Edwin Brady]

The point is that it *doesn't* pass type checking. It is intended that elemNilContra refl as you've written it doens't pass typechecking - that's what impossible verifies for you.

Edwin.

> --
> You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.
> For more options, visit https://groups.google.com/groups/opt_out.
>
>

[Chetan Taralekar]

Well, this can be used to prove anything!

Here's an example that typechecks with the latest version:

------------------------ CODE BEGINS

module Test

bot : (x : Nat) -> _|_

bot refl impossible

weird : _|_ -> (S O = O)

weird = FalseElim

wrong : (S O = O)

wrong = weird (bot O)

------------------------ CODE ENDS

[David Christiansen]

Hi Chetan,

Remember to mark your functions as total if you're using them as proofs. Partial functions that pass the type checker don't really count for proofs because they can be missing cases.

The totality checker isn't perfect, but in my experience it's quite helpful.

/David (from phone)

[Cezar Ionescu]

Chetan Taralekar <che...@gmail.com> wrote:

> Well, this can be used to prove anything!
>
> Here's an example that typechecks with the latest version:

Why the detour? Your code is equivalent to

> wrong : S O = O
> wrong refl impossible

Now, since no function is involved, marking |wrong| with |total| still
typechecks.

Best,
Cezar.

[Edwin Brady]

On 20 Mar 2013, at 07:05, David Christiansen <da...@davidchristiansen.dk> wrote:

> Hi Chetan,
>
> Remember to mark your functions as total if you're using them as proofs. Partial functions that pass the type checker don't really count for proofs because they can be missing cases.
>
> The totality checker isn't perfect, but in my experience it's quite helpful.

It's unfortunate that this is one of the situations where the coverage checker does the wrong thing! But yes, in general you should mark them as 'total' if you want to check your proof is complete.

Edwin.

[Edwin Brady]

On 20 Mar 2013, at 07:56, Cezar Ionescu <ion...@pik-potsdam.de> wrote:

>> wrong : S O = O
>> wrong refl impossible
>
> Now, since no function is involved, marking |wrong| with |total| still
> typechecks.

This should be rejected since you've attempted to give a definition, but shown there isn't one. It's a trivial fix (I think) so I will do that one.

It reminds me of a discussion last week of what the totality checker's behaviour should be when a function is not yet defined (i.e. it is a global metavariable). Should it reject the function because it's not there yet, or should it assume it is total so as not to affect checking of definitions that already exist (the current behaviour)? And does it really matter anyway since a program won't compile if there are missing definitions?

Edwin.