類型檢查的實例含義

我正在學習如何在Agda中實現「類型類」。作爲一個例子，我試圖實現羅馬數字，其組成與＃將進行類型檢查。類型檢查的實例含義

我不明白爲什麼阿格達抱怨沒有實例加入（羅馬_ _）（_羅馬_）_ - 顯然，它可能不知道是什麼的自然數代替那裏。

有沒有更好的方式來介紹羅馬數字，沒有「構造函數」形式？我有一個構造函數「madeup」，它可能需要是私有的，以確保我只有「可信」的方式通過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

顯然，如果我指定的隱明確，它的工作原理 - 所以我相信這不是那是錯的函數的類型。

來源

2013-08-18 Sassa NF

你的例子在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.

（source）

也就是說，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.

（source ）現在

，至於問題的第二部分：我不太確定你的最終目標是什麼，該代碼的結構最終取決於你想一旦你構建的數量做什麼。這就是說，我寫下了一個小程序，允許你輸入羅馬數字而不需要通過明確的數據類型（如果我沒有清楚地瞭解你的意圖，請原諒我）：

羅馬數字將是一個函數，它需要一對自然數 - 前一個數字的值和運行總數。如果它小於前面的數字，我們將從運行總數中減去它的值，否則我們將它加起來。我們返回當前數字的新運行總數和值。

當然，這並不完美，因爲沒有什麼可以阻止我們輸入I I X，我們最終將其評估爲10.我將這留作有興趣的讀者的練習。:)

進口第一（注意，我使用標準庫在這裏，如果你不想安裝它，你可以從the online repo複製定義）：

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 ⟧

評估通過C-c C-ntest₁給我們19，test₂然後14。

當然，您可以將這些不變式移動到數據類型中，添加新的不變量等等。

來源

2013-08-18 14:02:28 Vitus

很酷。我在2.3.0上，所以我可能需要升級，頭痛也會消失。 –

類型檢查的實例含義

回答

相關問題