类型检查的实例含义

我正在学习如何在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上，所以我可能需要升级，头痛也会消失。 –

类型检查的实例含义

回答

相关问题