Better detection of sized indexed types

[UlfNorell]

From fredrik....@gmail.com on September 26, 2012 16:28:16

Is there any reason why the subtyping introduced by --sized-types only works for unindexed types (parameters are okay)?

I tried the following on the darcs version from today (26/09/2012):

{-# OPTIONS --sized-types #-} {-# OPTIONS --show-implicit #-} module sizedsubtyping where

postulate Size : Set ↑_ : Size → Size ∞ : Size

{-# BUILTIN SIZE Size #-} {-# BUILTIN SIZESUC ↑_ #-} {-# BUILTIN SIZEINF ∞ #-}

record Top : Set where

data Param (A : Top) : {i : Size} -> Set where c : {i : Size} -> Param A {↑ i}

data Indexed : (A : Top) -> {i : Size} -> Set where c : {A : Top} -> {i : Size} -> Indexed A {↑ i}

works : {A : Top}{i : Size} -> Param A {i} -> Param A {↑ i} works x = x

fails : {A : Top}{i : Size} -> Indexed A {i} -> Indexed A {↑ i} fails x = x -- .i != ↑ .i of type Size -- when checking that the expression x has type -- Indexed (record { }) {↑ .i}

{- Trying to use the new Size< also fails -} postulate Size< : Size → Set {-# BUILTIN SIZELT Size< #-}

also-fails : {A : Top}{i : Size}{j : Size< i} -> Indexed A {j} -> Indexed A {i} also-fails x = x -- .j != .i of type Size -- when checking that the expression x has type -- Indexed (record { }) {.i}

also-works : {A : Top}{i : Size}{j : Size< i} -> Param A {j} -> Param A {i} also-works x = x

Original issue: http://code.google.com/p/agda/issues/detail?id=701

[UlfNorell]

From andreas....@gmail.com on September 26, 2012 13:14:25

The problem is that the sized-type detection is very narrow: Param is recognized as sized, but indexed not, because:

• the size index needs to be the first after the :
• the size variable needs to be quantified over first in the constructors.

So you have to write

data Indexed : {i : Size} -> Top -> Set c : {i : Size}{A : Top} -> Indexed {\up i} A

then it should work.

Of course, it is bad style to have a silent analysis that does not give feedback to the user. A pragma to mark a type as sized should be in order.

Status: InfoNeeded
Owner: andreas....@gmail.com

[UlfNorell]

From fredrik....@gmail.com on September 27, 2012 06:47:21

Thanks, that works!

I intuitively put the size index last after :, in the hope that this would make

Indexed A : {i : Size} -> Set

as similar to

Param A : {i : Size} -> Set

as possible. Is there any reason not to treat any inductive type indexed over Size as a sized type? Since Size is non-dependent, it should always be possible to reorder indices and arguments to pass the sized-type detection you mention, justifying this.

[UlfNorell]

From fredrik....@gmail.com on September 27, 2012 07:03:27

Another issue:

If I understand correctly, unconstrained sizes should be resolved to \infty. If I define

data U : {i : Size} -> Set where c : {i : Size} -> U {↑ i}

data V : {i : Size} -> Set where d : {i : Size} -> U {∞} -> V {↑ i}

works-with-explicit-infty : {i : Size} -> V {i} -> V {↑ i} works-with-explicit-infty x = x

everything is fine. However, if I leave out {\infty}:

data V' : {i : Size} -> Set where d : {i : Size} -> U -> V' {↑ i}

fails-if-no-infty : {i : Size} -> V' {i} -> V' {↑ i} fails-if-no-infty x = x --.i != ↑ .i of type Size --when checking that the expression x has type V'

V' is not detected as a sized type anymore which seems to break the promise about unconstrained sizes. Since U is just a non-inductive argument to d, I wouldn't expect it to influence whether V is a sized type or not?

[UlfNorell]

From andreas....@gmail.com on September 27, 2012 08:17:01

I fixed the bug described in comment 3. Comment 2 I take down as feature request.

Summary: Better detection of sized indexed types
Status: Accepted
Labels: Type-Enhancement Priority-Medium

[UlfNorell]

From andreas....@gmail.com on October 19, 2012 00:51:06

Probably this style of sized types will be removed at some time in favor of the sized types with Size<. So I have no plans to work on this soon.

Labels: -Priority-Medium Priority-Low

[UlfNorell]

From andreas....@gmail.com on October 19, 2012 00:52:03

Labels: -Sized-Types

[UlfNorell]

From andreas....@gmail.com on October 19, 2012 00:52:12

Labels: Sized-Types

[UlfNorell]

From andreas....@gmail.com on October 19, 2012 01:01:09

Labels: -Sized-Types SizedTypes