agda - 类型检查的实例隐式

Question

我正在学习如何在 Agda 中实现“类型类”。作为一个例子，我正在尝试实现罗马数字，其与 # 的组合将进行类型检查。

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

2. 有没有更好的方法来引入没有“构造函数”形式的罗马数字？我有一个构造函数“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
   

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

Answer 1