[Agda] Size Issue when Modelling Effectful Data Structures and Computations

[Jesper Cockx]

Hi Jonas,

If you can prove false, then it is reasonable to assume that you indeed
found a bug in the current version of Agda. Could you please report this
issue on the bug tracker at github.com/agda/agda/issues? Somehow the
unicode did not come through correctly which makes the code hard to read.

-- Jesper

On Tue, Sep 15, 2020 at 10:10 AM <jonas.hoefer at stud.htwk-leipzig.de> wrote:

> Hello
>
> > Note that the last example works fine:
>
> Your code only seems works with the current Agda version from the Master
> branch
> not Agda version 2.6.1 (or 2.6.1.1). I don't think the last example should
> work.
> It fails in version 2.6.1 with the error message "Set (suc a) is not less
> or
> equal than Set a".
>
> > foo bar : Free (Op a) (Listᴹ (Op a) Bool)
> > foo = pure nil
> > bar = op foo
>
> Op a produces a container of level suc a. Free and Listᴹ both use
> the level of
> their container i.e. suc a. op expects an argument of level a (not suc a,
> because the stored type is smaller), but passing foo seems to work.
>
> > op : {A : Set a} → Free (Op a) A → Free (Op a) A
> > op {A = A} ma = impure (opˢ A , λ { (inj₁ tt) →
> ma; (inj₂ x) → pure x })
>
> Replacing Set a with Set (suc a) in the definition of op fails with the
> same
> error, but the following works.
>
> > op′ : {a : Level} {A : Set (suc a)} → Free (Op a) A →
> Free (Op a) A
> > op′ {a} {A} ma = op {a} ma
>
> Passing {A} directly as an argument to op also yields the error, but
> omitting
> it works. I think this behavior is a bug in the current version, because
> the
> following implementation of Russel's paradox type checks with my build of
> the
> latest version (commit 832057961873856915c41745c37e055ff4b2c583).
>
>   {-# OPTIONS --cumulativity #-}
>
>   open import Data.Bool
>   open import Data.Empty
>   open import Data.Product
>   open import Data.Sum
>   open import Data.Unit
>   open import Data.Maybe
>
>   open import Function
>   open import Level
>
>   open import Relation.Binary.PropositionalEquality
>
>   private
>     variable
>       a : Level
>
>   record Container a : Set (suc a) where
>     constructor _◁_/_
>     field
>       Shape : Set a
>       Pos   : Shape → Set a
>       Ctx   : (s : Shape) → Pos s → Maybe {a = suc a} (Set a)
>
>   open Container public
>
>   ⟦_⟧ : Container a → (Set a → Set a) →
> Set a → Set a
>   ⟦ S ◁ P / C ⟧ F A = Σ[ s ∈ S ] ((p : P s)
> → F (fromMaybe A (C s p)))
>
>   data Free {a : Level} (C : Container a) (A : Set a) : Set a where
>     pure   : A                → Free C A
>     impure : ⟦ C ⟧ (λ A → Free C A) A →
> Free C A
>
>   data Listᴹ (C : Container a) (A : Set a) : Set a where
>     nil : Listᴹ C A
>     cons : Free C A → Free C (Listᴹ C A) → Listᴹ C
> A
>
>   ROp : ∀ a → Container (suc a)
>   ROp a = Set a ◁ id / λ _ _ → nothing
>
>   rop : {a : Level} {A : Set a} → Free (ROp a) A
>   rop {_} {A} = impure (A , pure)
>
>   rop′ : {a : Level} {A : Set (suc a)} → Free (ROp a) A
>   rop′ = rop
>
>   rop₁ : {A : Set₁} → Free (ROp 0ℓ) A
>   rop₁ = rop′
>
>   _bind_ : {A B : Set (suc a)} → Free (ROp a) A → (A →
> Free (ROp a) B)
>     → Free (ROp a) B
>   pure x bind k = k x
>   impure (X , pf) bind k = impure (X , λ p → pf p bind k)
>
>   M : Set₁
>   M = Free (ROp 0ℓ) ⊥
>
>   m : (I : Set₁) → (I → M) → M
>   m I pf = rop₁ {I} bind pf
>
>   -- Now we can follow some implementation of Russell's Paradox
>   -- http://www.cs.nott.ac.uk/~psztxa/g53cfr/l20.html/l20.html
>
>   _∈_ : M → M → Set₁
>   a ∈ (impure (I , f)) = ∃[ i ] (a ≡ f i)
>
>   _∉_ : M → M → Set₁
>   x ∉ y = x ∈ y → ⊥
>
>   R : M
>   R = m (Σ M λ s → s ∉ s) proj₁
>
>   lem-1 : {X : M} → X ∈ R → X ∉ X
>   lem-1 ((s , s∉s) , p) = subst₂ _∉_ p' p' s∉s
> where p' = sym p
>
>   lem-2 : {X : M} →  X ∉ X → X ∈ R
>   lem-2 {X} X∉X = ((X , X∉X) , refl)
>
>   lem-3 : R ∉ R
>   lem-3 R∈R = lem-1 R∈R R∈R
>
>   contr : ⊥
>   contr = lem-3 (lem-2 {R} lem-3)
>
> Jonas
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200915/26c369e9/attachment.html>