Agda 中实例参数的问题
Problems with instance arguments in Agda
我正在尝试遵循 McBride 的 How to Keep Your Neighbours in Order 代码,但无法理解为什么 Agda(我使用的是 Agda 2.4.2.2)给出以下错误消息:
Instance search can only be used to find elements in a named type
when checking that the expression t
has type .T
用于函数 _:-_
。代码如下
data Zero : Set where
record One : Set where
constructor <>
data Two : Set where tt ff : Two
So : Two -> Set
So tt = One
So ff = Zero
record <<_>> (P : Set) : Set where
constructor !
field
{{ prf }} : P
_=>_ : Set -> Set -> Set
P => T = {{ p : P }} -> T
infixr 3 _=>_
-- problem HERE!
_:-_ : forall {P T} -> << P >> -> (P => T) -> T
! :- t = t
非常感谢任何帮助。
Nils Anders Danielsson 最近在 agda-dev 邮件列表中有一封电子邮件正是关于此的。我在网上找不到,所以这里引用一下:
Conor uses lots of instance arguments in "How to Keep Your Neighbours
in Order". However, his code was written using the old variant of the
instance arguments, and fails to check now. I managed to make the code
work again using some small tweaks, and wonder if we could get away
with even less:
I replaced
record One : Set where constructor it
with
record One : Set where
instance
constructor it.
This seems fine with me.
I replaced
_:-_ : forall {P T} -> <P P P> -> (P => T) -> T
! :- t = t
with
_:-_ : forall {P T} -> <P P P> -> (P => T) -> T
! {{prf = p}} :- t = t {{p = p}},
because "Instance search can only be used to find elements in a
named type". Similarly, in two cases I replaced a module parameter
(L : REL P)
with
(L' : REL P) (let L = Named L'),
where Named is a named type family:
data Named {P : Set} (A : REL P) : REL P where
named : forall {x} -> A x -> Named A x
我正在尝试遵循 McBride 的 How to Keep Your Neighbours in Order 代码,但无法理解为什么 Agda(我使用的是 Agda 2.4.2.2)给出以下错误消息:
Instance search can only be used to find elements in a named type when checking that the expression
t
has type.T
用于函数 _:-_
。代码如下
data Zero : Set where
record One : Set where
constructor <>
data Two : Set where tt ff : Two
So : Two -> Set
So tt = One
So ff = Zero
record <<_>> (P : Set) : Set where
constructor !
field
{{ prf }} : P
_=>_ : Set -> Set -> Set
P => T = {{ p : P }} -> T
infixr 3 _=>_
-- problem HERE!
_:-_ : forall {P T} -> << P >> -> (P => T) -> T
! :- t = t
非常感谢任何帮助。
Nils Anders Danielsson 最近在 agda-dev 邮件列表中有一封电子邮件正是关于此的。我在网上找不到,所以这里引用一下:
Conor uses lots of instance arguments in "How to Keep Your Neighbours in Order". However, his code was written using the old variant of the instance arguments, and fails to check now. I managed to make the code work again using some small tweaks, and wonder if we could get away with even less:
I replaced
record One : Set where constructor it
with
record One : Set where instance constructor it.
This seems fine with me.
I replaced
_:-_ : forall {P T} -> <P P P> -> (P => T) -> T ! :- t = t
with
_:-_ : forall {P T} -> <P P P> -> (P => T) -> T ! {{prf = p}} :- t = t {{p = p}},
because "Instance search can only be used to find elements in a named type". Similarly, in two cases I replaced a module parameter
(L : REL P)
with
(L' : REL P) (let L = Named L'),
where Named is a named type family:
data Named {P : Set} (A : REL P) : REL P where named : forall {x} -> A x -> Named A x