Agda 级别错误消息的含义:... : .Agda.Primitive.Level [英] Meaning of Agda level error message: ... : .Agda.Primitive.Level

问题描述

我正在尝试破译有关级别的错误消息.在 Haskell 中，我可以以一种简单的方式编写以下流函数，twist:

I'm trying to decipher an error message concerning levels. In Haskell, I can write the following stream function, twist, in a straightforward fashion:

data Stream a = a :> Stream a
twist :: (a -> (b , (Either a c))) -> (c -> (b , (Either a c))) -> (Either a c) -> Stream b
twist lt rt (Left a) = b :> twist lt rt ac
   where
     (b , ac) = lt a
twist lt rt (Right c) = b :> twist lt rt ac
   where
     (b , ac) = rt c

到目前为止，一切都很好.现在，当我尝试在 Agda 中定义类似函数时，我收到一条关于我不理解的级别的错误消息.具体来说，我收到此错误消息:

So far, so good. Now, when I attempt to define the analogous function in Agda, I get an error message about levels that I don't understand. Specifically, I get this error message:

_a_41 : .Agda.Primitive.Level  [ at ...snip.../MinimalStream.agda:20,34-35 ]
_b_42 : .Agda.Primitive.Level  [ at ...snip.../MinimalStream.agda:20,34-35 ]

似乎是在抱怨twist的类型声明中类型变量a和b的级别，但我不确定我是否理解问题所在.任何人都可以提供的任何指示或解释将不胜感激！

It seems to be complaining about the level of type variables a and b in the type declaration of twist, but I am not sure I understand what the problem is. Any pointers or explanation that anyone could provide would be greatly appreciated!

谢谢，账单

这是生成完整精简版的 Agda 代码:

Here's the Agda code that generates thin its entirety:

module MinimalStream where

open import Data.Product using (_×_; _,_; proj₁)
open import Data.Sum -- using (_⊎_)

case_of_ : ∀ {a b} {A : Set a} {B : Set b} → A → (A → B) → B
case x of f = f x

record Stream A : Set where
  coinductive
  field headStr : A
        tailStr : Stream A
open Stream; S = Stream

-- standard kinds of stream functions work as expected.
unzip₁ : ∀ {a b : Set} → Stream (a × b) → Stream a
headStr (unzip₁ sab) = proj₁ (headStr sab)
tailStr (unzip₁ sab) = unzip₁ (tailStr sab)

twist : ∀ {a b c} → (a → (b × (a ⊎ c))) → (c → (b × (a ⊎ c))) → (a ⊎ c) → Stream b
headStr (twist lt rt (inj₁ a)) = case lt a of
                                    λ { (b , (inj₁ _)) → b ;
                                        (b , (inj₂ _)) → b }
headStr (twist lt rt (inj₂ c)) = case rt c of
                                    λ { (b , (inj₁ _)) → b ;
                                        (b , (inj₂ _)) → b }
tailStr (twist lt rt (inj₁ a)) = case lt a of
                                    λ { (_ , (inj₁ a')) → twist lt rt (inj₁ a') ;
                                        (_ , (inj₂ c))  → twist lt rt (inj₂ c)  }
tailStr (twist lt rt (inj₂ c)) = case rt c of
                                    λ { (_ , (inj₁ a))  → twist lt rt (inj₁ a) ;
                                        (_ , (inj₂ c')) → twist lt rt (inj₂ c')  }

推荐答案

欢迎使用 Stack Overflow！此类错误表示未解决的元变量，这意味着 Agda 未能推断出隐式参数.错误消息指示元变量的(自动生成的)名称及其类型.在这种情况下，问题可能出在 twist 中的 {a, b, c} 类型:目前尚不清楚这些应该处于哪个级别.要解决此问题，请指定级别:{ab c : Set}.

Welcome to Stack Overflow! This sort of error indicates an unsolved metavariable, which means that Agda has failed to infer an implicit argument. The error message indicates the metavariable's (autogenerated) name and its type. In this case, the issue is probably with the types {a, b, c} in twist: It is unclear which level these should be at. To fix this, specify the level: {a b c : Set}.

这篇关于Agda 级别错误消息的含义:... : .Agda.Primitive.Level的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！