Parameter order in function and "implicit" paramter

I'm really confused about implicit parameters. Namely in the b function/proof below.

In this video, which I'm trying to understand in-depth, I stumble on this point: we have the implicit {p} before the String s in the b {p} s binding definition.

b : (s : String) -> {p : Every BinChar (unpack s)} -> Nat
b {p} s = fromBinChars p (length s - 1)

I see that it compiles fine. But I was sort of expecting to have p in second position:

b s {p} = fromBinChars p (length s - 1)

or even (since p is implicit and already defined/assumed in the type signature)

b s = fromBinChars p (length s - 1)

Why is it not the case? What are the concepts that you think I'm misunderstanding?

This is the rest of the code:

data BinChar : Char -> Type where
  O : BinChar '0'
  1 : BinChar '1'

data Every : (a -> Type) -> List a -> Type where
  Nil : {P : a -> Type} -> Every P []
  (::) : {P : a -> Type} -> P x 
                         -> Every P xs
                         -> Every P (x :: xs)

fromBinChars : Every BinChar xs -> Nat -> Nat
fromBinChars [] k = k
fromBinChars (O :: z) k = fromBinChars xs (k - 1)
fromBinChars (I :: z) k = pow 2 k + fromBinChars xs (k - 1)

Solution

Your code contains quite a lot of errors. I do not know whether it is from typing it again into stackoverflow, or because of misreading the example from the video. AFAIK the idris version in the video is fairly old, and you also need to tweak your code a bit to get it running.

Here is a working example:

%default total
data BinChar : Char -> Type where
   O : BinChar '0'
   I : BinChar '1'

data Every : (a -> Type) -> List a -> Type where
   Nil : {P : a -> Type} -> Every P []
   (::) : {P : a -> Type} -> P x
                     -> Every P xs
                     -> Every P (x :: xs)

fromBinChars : Every BinChar xs -> Nat -> Nat
fromBinChars [] k = k
fromBinChars (O :: z) k = fromBinChars z (k `minus` 1)
fromBinChars (I :: z) k = pow 2 k `plus` fromBinChars z (k `minus` 1)

b : (s : String) -> {auto p : Every BinChar (unpack s)} -> Nat
b s {p} = fromBinChars p (length s `minus` 1)

test: b "101" = 5
test = Refl

Regarding your question 2) Why can't I just omit the implicit parameter and write b s = fromBinChars p (length s - 1)? This is fairly simple - in this case there is nothing on the right hand side which is called p. you need to introduce p on the left hand side.

Regarding your question 1) I guess keeping the order of the parameters would be considered good style and would usually be required as well. But idris seems to treat implicit parameters a bit different, so in this case it doesn't matter. But I would not bet on it. In this example I wouldn't assume that there is a real intention behind swapping the parameters.