隐式参数并不总是根据它的书面方式使用
我具有以下类型签名的功能：
loop : ∀ {x y z} → .⦃ _ : Rights y ⦄ → DRuby (⟨ x , y ⟩ , ⟨ y , z ⟩) → DRuby (x , z)
⟨_⟩表示法用于构造玫瑰树和权利y是一种数据结构，目睹某个属性保留一棵玫瑰树。
我通常必须编写.⦃_：权利y和。有点长，因此要缩短我想出的内容
infixr 5 R_⇒_
R_⇒_ : DShp → Set → Set
R x ⇒ y = .⦃ _ : Rights x ⦄ → y
，然后我可以像以上类型签名一样编写上述类型签名
loop : ∀ {x y z} → R y ⇒ DRuby (⟨ x , y ⟩ , ⟨ y , z ⟩) → DRuby (x , z)
，在某些情况下，具有的原始版本。 ry⇒无法打字 - 我会发现无法求解约束/解决实例参数的错误。此外，我无法在实例参数上进行模式匹配：
loop {x} {y} {z} ⦃ p ⦄ q = ?
给出错误
Unexpected implicit argument
when checking that the clause
loop {x} {y} {z} ⦃ p ⦄ q = ?
has type
{x : Rose (Type × Dir)} {y : _B_1266 x} {z : Rose (Type × Dir)} →
R x ⇒ DRuby (RS.⟨ _r_1261 ⟩ (x , y) , RS.⟨ _r_1269 ⟩ (y , z)) →
DRuby (x , z)
，但是还有许多其他函数，它可以通过ry⇒ toge -typecheck（如果我删除它，则不会打字，因此正在使用）。
我想我的问题是双重的：
是否期望行为是在定义
r_⇒_之类的函数时，我无法在内容上进行模式匹配，有时候，内容在期间找不到实例搜索？有没有一种方法可以使函数/同义词/宏（例如
r_⇒_）正确工作？例如，像c宏那样只是文字替换吗？
I have a function with the following type signature:
loop : ∀ {x y z} → .⦃ _ : Rights y ⦄ → DRuby (⟨ x , y ⟩ , ⟨ y , z ⟩) → DRuby (x , z)
where the ⟨_⟩ notation is for constructing rose trees and Rights y is a data structure that witnesses that a certain property holds for a rose tree.
I often have to write .⦃ _ : Rights y ⦄ and .⦃ _ : Lefts y ⦄, sometimes multiple of these in a single type signature, and it starts to get a bit long, so to shorten things I came up with
infixr 5 R_⇒_
R_⇒_ : DShp → Set → Set
R x ⇒ y = .⦃ _ : Rights x ⦄ → y
and then I can write the above type signature as
loop : ∀ {x y z} → R y ⇒ DRuby (⟨ x , y ⟩ , ⟨ y , z ⟩) → DRuby (x , z)
However, in some cases the original version with .⦃ _ : Rights y ⦄ works but the version with R y ⇒ fails to typecheck - I get errors about failing to solve constraints/resolve instance arguments. Furthermore, I am unable to pattern match on the instance argument:
loop {x} {y} {z} ⦃ p ⦄ q = ?
gives the error
Unexpected implicit argument
when checking that the clause
loop {x} {y} {z} ⦃ p ⦄ q = ?
has type
{x : Rose (Type × Dir)} {y : _B_1266 x} {z : Rose (Type × Dir)} →
R x ⇒ DRuby (RS.⟨ _r_1261 ⟩ (x , y) , RS.⟨ _r_1269 ⟩ (y , z)) →
DRuby (x , z)
But there are a number of other functions where it typechecks just fine with R y ⇒ (and doesn't typecheck if I remove it, so it is being used).
I suppose my question is twofold:
Is it expected behaviour that when defining a function like
R_⇒_I can't pattern match on the contents, and that sometimes the contents aren't found during instance search?Is there a way to make a function/synonym/macro like
R_⇒_that works properly? For example, something like a C macro that is just a textual substitution?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
感谢@Jesper为我解决问题：
→具有所有操作员的最低优先级，因为它是由解析器直接处理的，而不是被解析为符号并稍后分解为操作员。结果，a * b→c等任何代码，其中*是二进制操作，将被解析为（a * b）→C，无论您给出*什么优先级。在这种情况下，它解析rx⇒y→zas（rx⇒y）→z，这意味着权利x不能在y中使用。解决方案是添加括号：rx⇒（y→z）。Thanks to @Jesper for solving the problem for me:
→has the lowest precedence of all operators as it is handled directly by the parser rather than parsed as a symbol and resolved into an operator later. As a result, any piece of code likea * b → c, where*is a binary operation, will be parsed as(a * b) → c, no matter what precedence you give*. In this case it parsesR x ⇒ y → zas(R x ⇒ y) → z, which means thatRights xcan't be used except iny. The solution is to add parentheses:R x ⇒ (y → z).