agda - 型チェックのためのインスタンスの暗黙

Question

Agdaで「型クラス」がどのように実装されているかを学んでいます。例として、 # を使用した構成が型チェックになるローマ数字を実装しようとしています。

1. Join (Roman _ _) (Roman _ _) _ のインスタンスがないと Agda が不平を言う理由がよくわかりません。

2. 「コンストラクタ」形式を持たないローマ数字を導入するより良い方法はありますか? 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