代码之家 › 专栏 › 技术社区 › Stephane Rolland

函数中的参数顺序和“隐式”参数

function-parameter idris implicit

Stephane Rolland · 技术社区 · 6 年前

我真的对隐式参数感到困惑。即在 b 功能/证明如下。

在这个里面 video 我正试图深入理解这一点,我无意中发现了这一点:我们有 {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)

1 回复 | 直到 6 年前

Markus 6 年前

您的代码包含很多错误。我不知道是因为它再次输入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,你需要介绍一下 p 在左手边。

关于你的问题1) 我想保持参数的顺序将被认为是好的样式,并且通常也是必需的。但idris似乎对待隐式参数有点不同,所以在本例中并不重要。但我不赌。在这个例子中,我不认为交换参数背后有真正的意图。