Последствия экземпляра для проверки типа

Я изучаю, как в Agda реализованы «классы типов». В качестве примера я пытаюсь реализовать римские цифры, композиция которых с # будет проверять тип.

  1. Я не понимаю, почему Agda жалуется, что нет экземпляра для Join (Roman _ _) (Roman _ _) _ - очевидно, он не мог понять, какие натуральные числа там подставлять.

  2. Есть ли лучший способ ввести римские числа, не имеющие формы «конструктор»? У меня есть конструктор «madeup», который, вероятно, должен быть частным, чтобы быть уверенным, что у меня есть только «надежные» способы создания других римских чисел через соединение.

    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
person Sassa NF    schedule 18.08.2013    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Ваш пример отлично работает в разрабатываемой версии 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.

(исходный код)

То есть до 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.

(исходный код)

Теперь, что касается второй части вопроса: я не совсем уверен, какова ваша конечная цель, структура кода в конечном итоге зависит от того, что вы хотите сделать после создания числа. При этом я написал небольшую программу, которая позволяет вам вводить римские цифры, не просматривая явный тип данных (простите меня, если я не уловил вашего намерения ясно):

Римская цифра будет функцией, которая принимает пару натуральных чисел - значение предыдущей цифры и промежуточную сумму. Если оно меньше предыдущего числа, мы вычтем его значение из промежуточной суммы, в противном случае мы добавим его. Возвращаем новый нарастающий итог и значение текущего числа.

Конечно, это далеко не идеально, потому что ничто не мешает нам набрать I I X, и в итоге мы оцениваем его как 10. Я оставляю это как упражнение для заинтересованного читателя. :)

Сначала импорт (обратите внимание, что здесь я использую стандартную библиотеку, если вы не хотите ее устанавливать, вы можете просто скопировать определение из онлайн-репо):

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

Это наша цифровая фабрика:

_<?_ : 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 ⟧

Оценка test₁ через C-c C-n дает нам 19, test₂, затем 14.

Конечно, вы можете переместить эти инварианты в тип данных, добавить новые инварианты и так далее.

person Vitus    schedule 18.08.2013
comment
Прохладный. Я использую 2.3.0, поэтому, возможно, мне нужно обновить систему, и головная боль исчезнет. - person Sassa NF; 18.08.2013