Порядок параметров в функции и «неявный» параметр

Question

Я действительно запутался в неявных параметрах.А именно в b функции / доказательстве ниже.

В этом видео , которое я пытаюсь глубоко понять, я натыкаюсь на этот момент: у нас есть неявное {p} до String s в определении связывания b {p} s.

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

Я вижу, что он прекрасно компилируется.Но я ожидал, что p будет на второй позиции:

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

или даже (поскольку p неявно и уже определено / предполагается в сигнатуре типа)

b s = fromBinChars p (length s - 1)

Почему это не так?Какие концепции, по вашему мнению, я неправильно понимаю?

Это остальная часть кода:

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)  

Answer 1

Ваш код содержит довольно много ошибок.Я не знаю, является ли это повторным вводом его в stackoverflow или из-за неправильного прочтения примера из видео.AFAIK Версия idris в видео довольно старая, и вам также нужно немного настроить свой код, чтобы запустить его.

Вот рабочий пример:

%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

Относительно вашего вопроса2) Почему я не могу просто пропустить неявный параметр и написать b s = fromBinChars p (length s - 1)?Это довольно просто - в этом случае справа нет ничего, что называется р.вам нужно ввести p с левой стороны.

Относительно вашего вопроса 1) Я думаю, сохранение порядка параметров будет считаться хорошим стилем и, как правило, также потребуется.Но idris, похоже, обрабатывает неявные параметры немного по-другому, поэтому в этом случае это не имеет значения.Но я бы не стал на это ставить.В этом примере я бы не предположил, что за изменением параметров стоит реальное намерение.