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

[Nils Anders Danielsson]

On 2020-09-12 14:11, jonas.hoefer at stud.htwk-leipzig.de wrote:
> Please correct me if I'm wrong about the increasing levels. I did some
> more experiments and wrote up another sketch using universe
> polymorphism. It's probably not the cleanest implementation of the
> idea, but it demonstrates some consequences.
> 
> https://gist.github.com/JonasHoefer/0e3940b8c2a7264fde06aea5ddd967c0

In that code you use Setω. I took your first example and made it
universe-polymorphic in a more normal way. Note that the last example
works fine:

   {-# OPTIONS --cumulativity #-}

   open import Data.Bool
   open import Data.Product
   open import Data.Sum
   open import Data.Unit
   open import Data.Maybe
   open import Level

   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 (C : Container a) (A : Set a) : Set a where
     pure   : A                → Free C A
     impure : ⟦ C ⟧ (Free C) 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

   data OpShape a : Set (suc a) where
     opˢ : (X : Set a) → OpShape a

   OpPos : OpShape a → Set a
   OpPos (opˢ X) = ⊤ ⊎ X

   OpCtx : (s : OpShape a) → OpPos s → Maybe (Set (suc a))
   OpCtx (opˢ X) (inj₁ tt) = just X
   OpCtx (opˢ X) (inj₂ x)  = nothing

   Op : ∀ a → Container (suc a)
   Op a = OpShape a ◁ OpPos / OpCtx

   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 })

   foo bar : Free (Op a) (Listᴹ (Op a) Bool)
   foo = pure nil
   bar = op foo

-- 
/NAD