类型检查的实例隐式答案

【问题标题】：Instance Implicits for Type Checking类型检查的实例隐式
【发布时间】：2013-08-18 08:18:35
【问题描述】：

我正在学习如何在 Agda 中实现“类型类”。例如，我正在尝试实现带有 # 的组合会进行类型检查的罗马数字。

我不清楚为什么 Agda 抱怨没有 Join (Roman _ _) (Roman _ _) _ 的实例 - 显然，它无法计算出在那里替换的自然数。

有没有更好的方法来引入没有“构造函数”形式的罗马数字？我有一个构造函数“makeup”，它可能需要是私有的，以确保我只有“可信”的方式来通过 Join 构造其他罗马数字。

module Romans where

  data ℕ : Set where
    zero : ℕ
    succ : ℕ → ℕ

  infixr 4 _+_ _*_ _#_

  _+_ : ℕ → ℕ → ℕ
  zero + x = x
  succ y + x = succ (y + x)

  _*_ : ℕ → ℕ → ℕ
  zero * x = zero
  succ y * x = x + (y * x)

  one = succ zero

  data Roman : ℕ → ℕ → Set where
    i : Roman one one
{-    v : Roman one five
    x : Roman ten one
... -}
    madeup : ∀ {a b} (x : Roman a b) → (c : ℕ) → Roman a c

  record Join (A B C : Set) : Set where
    field jo : A → B → C

  two : ∀ {a} → Join (Roman a one) (Roman a one) (Roman a (one + one))
  two = record { jo = λ l r → madeup l (one + one) }

  _#_ : ∀ {a b c d C} → {{j : Join (Roman a b) (Roman c d) C}} → Roman a b → Roman c d → C
  (_#_) {{j}} = Join.jo j

  --   roman = (_#_) {{two}} i i -- works
  roman : Roman one (one + one)
  roman = {! i # i!} -- doesn't work

显然，如果我明确指定隐式，它会起作用 - 所以我相信这不是函数的类型错误。

【问题讨论】：

标签： agda

【解决方案1】：

您的示例在 Agda 的开发版本中运行良好。如果您使用的是 2.3.2 之前的版本，发行说明中的这段话可以阐明为什么它不能为您编译：

* Instance arguments resolution will now consider candidates which
  still expect hidden arguments. For example:

    record Eq (A : Set) : Set where
      field eq : A → A → Bool

    open Eq {{...}}

    eqFin : {n : ℕ} → Eq (Fin n)
    eqFin = record { eq = primEqFin }

    testFin : Bool
    testFin = eq fin1 fin2

  The type-checker will now resolve the instance argument of the eq
  function to eqFin {_}. This is only done for hidden arguments, not
  instance arguments, so that the instance search stays non-recursive.

(source)

也就是说，在 2.3.2 之前，实例搜索将完全忽略您的 two 实例，因为它有一个隐藏的参数。

虽然实例参数的行为有点像类型类，但请注意，如果范围内只有一个类型正确的版本，它们只会提交给实例，并且它们不会执行递归搜索：

  Instance argument resolution is not recursive. As an example,
  consider the following "parametrised instance":

    eq-List : {A : Set} → Eq A → Eq (List A)
    eq-List {A} eq = record { equal = eq-List-A }
      where
      eq-List-A : List A → List A → Bool
      eq-List-A []       []       = true
      eq-List-A (a ∷ as) (b ∷ bs) = equal a b ∧ eq-List-A as bs
      eq-List-A _        _        = false

  Assume that the only Eq instances in scope are eq-List and eq-ℕ.
  Then the following code does not type-check:

    test = equal (1 ∷ 2 ∷ []) (3 ∷ 4 ∷ [])

  However, we can make the code work by constructing a suitable
  instance manually:

    test′ = equal (1 ∷ 2 ∷ []) (3 ∷ 4 ∷ [])
      where eq-List-ℕ = eq-List eq-ℕ

  By restricting the "instance search" to be non-recursive we avoid
  introducing a new, compile-time-only evaluation model to Agda.

(source)

现在，至于问题的第二部分：我不确定您的最终目标是什么，代码的结构最终取决于您构建数字后想要做什么。话虽如此，我写了一个小程序，允许您输入罗马数字而无需通过显式数据类型（如果我没有清楚地理解您的意图，请原谅我）：

罗马数字将是一个函数，它采用一对自然数 - 前一个数字的值和运行总数。如果它小于之前的数字，我们将从运行总数中减去它的值，否则我们将其相加。我们返回新的运行总计和当前数字的值。

当然，这远非完美，因为没有什么可以阻止我们输入I I X，我们最终将其评估为 10。我将其作为练习留给感兴趣的读者。 :)

先导入（注意我这里使用的是标准库，如果不想安装，可以直接从the online repo复制定义）：

open import @987654324@
open import @987654325@
open import @987654326@
open import @987654327@
open import @987654328@

这是我们的数字工厂：

_<?_ : Decidable _<_
m <? n = suc m ≤? n

makeNumeral : ℕ → ℕ × ℕ → ℕ × ℕ
makeNumeral n (p , c) with ⌊ n <? p ⌋
... | true  = n , c ∸ n
... | false = n , c + n

我们可以制作几个数字：

infix 500 I_ V_ X_

I_ = makeNumeral 1
V_ = makeNumeral 5
X_ = makeNumeral 10

接下来，我们必须将这个函数链应用到某个东西上，然后提取运行总数。这不是最好的解决方案，但在代码中看起来不错：

⟧ : ℕ × ℕ
⟧ = 0 , 0

infix 400 ⟦_

⟦_ : ℕ × ℕ → ℕ
⟦ (_ , c) = c

最后：

test₁ : ℕ
test₁ = ⟦ X I X ⟧

test₂ : ℕ
test₂ = ⟦ X I V ⟧

通过C-c C-n评估test₁给我们19，test₂然后14。

当然，您可以将这些不变量移到数据类型中，添加新的不变量等等。

【讨论】：

酷。我在 2.3.0，所以可能我需要升级，头痛就会消失。