Я пытаюсь расшифровать сообщение об ошибке, касающееся уровней.В Haskell я могу написать следующую потоковую функцию, скручивая, простым способом:
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, я получаю сообщение об ошибке об уровнях, которые я не понимаю.В частности, я получаю это сообщение об ошибке:
_a_41 : .Agda.Primitive.Level [ at ...snip.../MinimalStream.agda:20,34-35 ]
_b_42 : .Agda.Primitive.Level [ at ...snip.../MinimalStream.agda:20,34-35 ]
Кажется, что он жалуется на уровень переменных типа a и b в объявлении типа twist, но я не уверен, что понимаю, в чем проблема.Будем весьма благодарны за любые указания или объяснения, которые кто-либо может предоставить!
Спасибо, Билл
Вот код Agda, который генерирует тонкий код целиком:
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') }