Trying to understand type check failure

[Jason Dagit]

Hello,

To explore idris I started typing some Haskell examples. I don't
expect them to work necessarily due to the difference between lazy and
eager evaluation. My goal is simply to learn more about idris.

Here are my examples:

$ cat examples.idr
import prelude.list

total
zipWith : (a -> b -> c) -> List a -> List b -> List c
zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
zipWith _ _ _ = Nil

total
almostfibs : List Int
almostfibs = 0 :: 1 :: zipWith (+) almostfibs almostfibs

total
fibs : List Int
fibs = 0 :: 1 :: zipWith (+) fibs (tail fibs)

almostfibs and fibs give very different errors when checked:

$ idris --check examples.idr
examples.idr:14:Can't unify Vect a n with List b

Specifically:
Can't unify Vect a with List
examples.idr:10:almostfibs is possibly not total as it is not well founded

Since I don't actually mention a Vect anywhere, why does fibs (which
only differs by the call to tail) cause this specific type error?

Thanks,
Jason

[Dominic Mulligan]

Hi,

In lib/prelude/list.idr the function tail has the following type:

total tail : (l : List a) -> (isCons l = True) -> List a
tail (x::xs) = ...

In other words both a list and a proof that the list is non-empty need
to be supplied in order to be able to use tail. I think lib/prelude/
vect.idr also exports a tail function which does not require a proof,
due to the typing of the Vect data type, and it probably gets brought
into scope by default as it is part of the Prelude. Is fibs really
what you want? Idris is strict be default.

Cheers,
Dom

[Dominic Mulligan]

By the way, if you get problems with names being seemingly brought
into scope at random, then you can start Idris with

idris --noprelude <file.idr>

to stop the Prelude being imported automatically, and see whether this
fixes the problem.

Cheers,
Dom

[Edwin Brady]

On 16 Feb 2012, at 07:24, Jason Dagit wrote:

> Since I don't actually mention a Vect anywhere, why does fibs (which
> only differs by the call to tail) cause this specific type error?

This is because the constructors for List and Vec are overloaded, as are several functions. Overloading is resolved by type, and if there's a type error with all possible overloadings, idris will attempt to guess which one was most likely.
Looks like it didn't guess successfully here... the heuristic doesn't look at the context, and it probably should.

The problem is that tail for lists requires a second argument which proves that the list is not empty. I think the number of arguments is the reason the error message guessed you mean vect.tail. Fortunately, it's easy to prove here. I have:

fibs : List Int
fibs = 0 :: 1 :: zipWith (+) fibs (tail fibs ?fibtail)

---------- Proofs ----------

fibtail = proof {
intros;
trivial;
}

*example> show $ take 10 fibs
"[0, 1, 1, 2, 3, 5, 8, 13, 21, 34]" : String

(This only works because the evaluator at the prompt is written in Haskell and thus lazy... also because I fixed a mistake in take/drop, which is now in git. Oops :))

Edwin.

[Jason Dagit]

On Thu, Feb 16, 2012 at 1:48 AM, Dominic Mulligan
<dominic.p...@googlemail.com> wrote:
> Hi,
>
> In lib/prelude/list.idr the function tail has the following type:
>
> total tail : (l : List a) -> (isCons l = True) -> List a
> tail (x::xs) = ...
>
> In other words both a list and a proof that the list is non-empty need
> to be supplied in order to be able to use tail.

Okay. I wondered about that definition. There isn't an explicit
argument for the proof and I haven't read yet how idris does these
sorts of things.

> I think lib/prelude/
> vect.idr also exports a tail function which does not require a proof,
> due to the typing of the Vect data type, and it probably gets brought
> into scope by default as it is part of the Prelude.

I see.

> Is fibs really
> what you want?  Idris is strict be default.

Yes, I just want to use familiar definitions to explore idris at the
moment. I knew I wouldn't be able to run that example.

Thanks,
Jason

[Jason Dagit]

On Thu, Feb 16, 2012 at 3:42 AM, Edwin Brady <edwin...@gmail.com> wrote:
> On 16 Feb 2012, at 07:24, Jason Dagit wrote:
>
>> Since I don't actually mention a Vect anywhere, why does fibs (which
>> only differs by the call to tail) cause this specific type error?
>
> This is because the constructors for List and Vec are overloaded, as are several functions. Overloading is resolved by type, and if there's a type error with all possible overloadings, idris will attempt to guess which one was most likely.
> Looks like it didn't guess successfully here... the heuristic doesn't look at the context, and it probably should.

Perhaps you can do what g++ does with C++ overloading. Explain (in the
error) why the "best candidate" was not suitable and then list the
other candidates.

>
> The problem is that tail for lists requires a second argument which proves that the list is not empty. I think the number of arguments is the reason the error message guessed you mean vect.tail. Fortunately, it's easy to prove here. I have:

Thanks for the example. I will study it.

>
> fibs : List Int
> fibs = 0 :: 1 :: zipWith (+) fibs (tail fibs ?fibtail)
>
> ---------- Proofs ----------
>
> fibtail = proof {
>    intros;
>    trivial;
> }
>
> *example> show $ take 10 fibs
> "[0, 1, 1, 2, 3, 5, 8, 13, 21, 34]" : String
>
> (This only works because the evaluator at the prompt is written in Haskell and thus lazy... also because I fixed a mistake in take/drop, which is now in git. Oops :))

Oh interesting semantic difference between the prompt and compiled.
Did you know that when SBCL forked from CMU's lisp the threw away the
interpreter and in the repl they compiled everything and then ran it?
They found it allowed them to be rid of many bugs where the
interpreter behaved subtly different from the compiler. I realize
idris is still very young, but it's a technique you might keep in mind
for when you have a chance to implement it :)

Thanks,
Jason

[Dominic Mulligan]

Hi,

> Okay.  I wondered about that definition. There isn't an explicit
> argument for the proof and I haven't read yet how idris does these
> sorts of things.

The full definition of tail is here (the definition in my last e-mail
was faulty, as I was typing it out from memory):

tail : (l : List a) -> (isCons l = True) -> List a

tail (x::xs) p = xs

There is an explicit argument for the proof here, it's p.

Thanks,
Dom

[Jason Dagit]

Silly me in that case.

Jason

[Edwin Brady]

On 16 Feb 2012, at 18:31, Jason Dagit wrote:

>> (This only works because the evaluator at the prompt is written in Haskell and thus lazy... also because I fixed a mistake in take/drop, which is now in git. Oops :))
>
> Oh interesting semantic difference between the prompt and compiled.
> Did you know that when SBCL forked from CMU's lisp the threw away the
> interpreter and in the repl they compiled everything and then ran it?
> They found it allowed them to be rid of many bugs where the
> interpreter behaved subtly different from the compiler. I realize
> idris is still very young, but it's a technique you might keep in mind
> for when you have a chance to implement it :)

At the minute, it's just more convenient for them to be separate, but it would be a good idea to unify them eventually. What I'd actually like to do is something along these lines:

http://gallium.inria.fr/~xleroy/publi/strong-reduction.pdf

(i.e. tweak the compiler so that it's usable by unification/conversion checking too.)

Edwin.