Как бороться с конфликтующими определениями модулей? - PullRequest
Новая
       7

Как бороться с конфликтующими определениями модулей?

0 голосов
/ 31 октября 2019 
open import Data.Vec
open import Data.Nat
open import Data.Fin
open import Data.Integer
open import Data.Rational
open import Data.Product
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

Infoset = ℕ
Size = ℕ
Player = ℤ

data GameTree (infoset-size : Infoset → Size) : Set where
  Terminal : (reward : ℚ) → GameTree infoset-size
  Response : (id : Infoset) → (subnodes : Vec (GameTree infoset-size) (infoset-size id)) → GameTree infoset-size

record Policy (infoset-size : Infoset → Size) : Set where
  field
    σ : ∀ (id : Infoset) → Vec ℚ (infoset-size id)
    wf-elem : ∀ (id : Infoset) (i : Fin (infoset-size id)) → 0ℚ Data.Rational.≤ lookup (σ id) i × lookup (σ id) i Data.Rational.≤ 1ℚ

Если бы я написал выше, как 0ℚ ≤ lookup (σ id) i × lookup (σ id) i ≤ 1ℚ Я получил бы следующую ошибку типа. 

Ambiguous name _≤_. It could refer to any one of
  Data.Nat._≤_ bound at
    C:\Users\Marko\AppData\Roaming\cabal\x86_64-windows-ghc-8.6.5\Agda-2.6.0\lib\agda-stdlib\src\Data\Nat\Base.agda:33,6-9
  Data.Fin._≤_ bound at
    C:\Users\Marko\AppData\Roaming\cabal\x86_64-windows-ghc-8.6.5\Agda-2.6.0\lib\agda-stdlib\src\Data\Fin\Base.agda:218,1-4
  Data.Integer._≤_ bound at
    C:\Users\Marko\AppData\Roaming\cabal\x86_64-windows-ghc-8.6.5\Agda-2.6.0\lib\agda-stdlib\src\Data\Integer\Base.agda:44,6-9
  Data.Rational._≤_ bound at
    C:\Users\Marko\AppData\Roaming\cabal\x86_64-windows-ghc-8.6.5\Agda-2.6.0\lib\agda-stdlib\src\Data\Rational\Base.agda:71,6-9

Есть ли какой-нибудь элегантный способ заставить Agda сделать вывод о правильных функциях для использования насвой? Здесь он должен быть способен делать правильные вещи, учитывая, что типы известны.

1 Ответ

2 голосов
/ 01 ноября 2019

Agda допускает неоднозначные конструкторы и неоднозначные проекции, но любые другие имена должны быть однозначными в том месте, где они используются.

Чтобы избежать неоднозначности, вы можете переименовать символ, используя синтаксис open import Data.Nat renaming (_≤_ to _≤Nat_). В качестве альтернативы вы можете использовать open import Data.Nat as Nat и x Nat.≤ y.

. В другой конструкции библиотеки может использоваться аргументы экземпляра для обеспечения специальной перегрузки (например, Agda). прелюдия ).

...