Instance Implicits for Type Checking

Question

I am learning how "typeclasses" are implemented in Agda. As an example, I am trying to implement Roman numerals whose composition with # would type-check.

1. I am not clear why Agda complains there is no instance for Join (Roman _ _) (Roman _ _) _ - clearly, it couldn't work out what natural numbers to substitute there.

2. Is there a nicer way to introduce Roman numbers that don't have "constructor" form? I have a constructor "madeup", which probably would need to be private, to be sure I have only "trusted" ways to construct other Roman numbers through 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
   

Clearly, if I specify the implicit explicitly, it works - so I am confident it is not the type of the function that is wrong.

Answer 1

Your example works fine in development version of Agda. If you are using a version older than 2.3.2, this passage from release notes could clarify why it doesn't compile for you:

* 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)

That is, before 2.3.2, the instance search would completly ignore your two instance because it has a hidden argument.

While instance arguments behave a bit like type classes, note that they will only commit to an instance if there's only one type correct version in scope and they will not perform a recursive search:

  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)

---

Now, as for the second part of the question: I'm not exactly sure what your final goal is, the structure of the code ultimately depends on what you want to do once you construct the number. That being said, I wrote down a small program that allows you to enter roman numerals without going through the explicit data type (forgive me if I didn't catch your intent clearly):

A roman numeral will be a function which takes a pair of natural numbers - the value of previous numeral and the running total. If it's smaller than previous numeral, we'll subtract its value from the running total, otherwise we add it up. We return the new running total and value of current numeral.

Of course, this is far from perfect, because there's nothing to prevent us from typing I I X and we end up evaluating this as 10. I leave this as an exercise for the interested reader. :)

Imports first (note that I'm using the standard library here, if you do not want to install it, you can just copy the definition from the online repo):

open import Data.Bool
open import Data.Nat
open import Data.Product
open import Relation.Binary
open import Relation.Nullary.Decidable

This is our numeral factory:

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

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

And we can make a few numerals:

infix 500 I_ V_ X_

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

Next, we have to apply this chain of functions to something and then extract the running total. This is not the greatest solution, but it looks nice in code:

⟧ : ℕ × ℕ
⟧ = 0 , 0

infix 400 ⟦_

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

And finally:

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

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

Evaluating test₁ via C-c C-n gives us 19, test₂ then 14.

Of course, you can move these invariants into the data type, add new invariants and so on.