[Agda-dev] Using the size solver to get proto-cumulativity

[Guillaume Allais]

Hi all,

Bounded level polymorphism would be amazing for stuff like IO.
At the moment we have this coinductive definition which mandates
that all actions live at the same level:

data IO {a} (A : Set a) : Set (suc a) where
  lift   : (m : Prim.IO A) → IO A
  return : (x : A) → IO A
  _>>=_  : {B : Set a} (m : ∞ (IO B)) (f : (x : B) → ∞ (IO A)) → IO A
  _>>_   : {B : Set a} (m₁ : ∞ (IO B)) (m₂ : ∞ (IO A)) → IO A

Because the primitive actions in the stdlib are defined at zero,
this means that everything needs to be at level 0 (or you need
to define your own new level-polymorphic versions of the primitives
by going back to the low-level IO.Primitive internals).

Ideally you'd indeed want (note that I'd prefer `Set<` to `Set<=`
as this would allow us to make `IO` an endofunctor on `Set a`
which would make it fit inside the `RawMonad` interface):

data IO {a} (A : Set a) : Set a where
  lift   : (m : Prim.IO A) → IO A
  return : (x : A) → IO A
  _>>=_  : {B : Set< a} (m : ∞ (IO B)) (f : (x : B) → ∞ (IO A)) → IO A
  _>>_   : {B : Set< a} (m₁ : ∞ (IO B)) (m₂ : ∞ (IO A)) → IO A

I have no idea about the added complexity in terms of inference
though. I just know I'd love to have something like this! :D

Cheers,
--
gallais

On 26/06/18 00:36, peio borthelle wrote:
> Hi, new here! This is a follow-up from irc (i'm lapinot).
>
> So basically i wondered if it had already been investigated to give levels the same
> kind of interface as the current sizes (and if it has, what are the pitfalls). To
> explain a bit more what i mean, the crucial point is probably having a subtyping
> relationship but only for levels. I guess it would look like:
>
> postulate
>   LevelUniv : LevelUniv
>   Level : LevelUniv
>   Level<= : Level -> LevelUniv
>   lzero : Level
>   lsuc : Level -> Level
>   lub : Level -> Level -> Level
>
> Together with a subtyping relationships `if a <= b, Level<= a <: Level<= b`, `if a :
> Level, a : Level<= a` and `LevelUniv <: Set`. I guess that we could then create a
> type of explicitely cumulative sets:
>
> CSet : (a : Level) -> Set (lsuc a)
> CSet a = Sigma (Level<= a) (\ b -> Set b)
>
> Incidentally we could also get rid of the most annoying instances of `Lift`-hell that
> arise when trying to give smaller than intended sets as parameters to some structure.
>
> data Ugly (a : Level) : Set (lsuc a) where
>   con : Set a -> Foo
>
> -- throws in wrapping/unwrapping, clutters the output type (affects next definitions)
> ugly : {a b} -> Set a -> Ugly (a lub b)
> ugly X = con (Lift X)
>
> -- no wrapping, clean interface
> data Nice (a : Level) : Set (lsuc a) where
>   con : {b : Level<= a} -> Set b -> Foo
>
>
> Note that this whole thing may be actually hard if the generated constraints are hard
> to solve, but until now i failed to see how they could be different than the one for
> the sizes. There was some point about uniqueness of the solutions, i'm not sure how
> this is handled by the sizes (is size uniqueness required?). Yet it might be pretty
> reasonable to select the smallest solution.
>
> If this approach works, it may be interesting to unify sizes and levels to a more
> abstract ordinal (heck we might even add `lim : (a : Ord) -> (Ord< a -> Ord) ->
> Ord`!). I guess that nothing stops us from using the same type to index sets (which
> is already a core language type, thus magic) and to help solving termination.
>
> Cheers,
> peio
> _______________________________________________
> Agda-dev mailing list
> Agda-dev at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda-dev


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda-dev/attachments/20180626/9a57e993/attachment.sig>