[Agda] generic type recursion

[Daniel Peebles]

Nothing is constraining your recursive OrderedNatList? call to have the
same DecTotalOrder as its implicit parameter, and the only part of that
that appears explicitly is the Carrier (which couldn't be injective even if
Agda did have some notion of that, because the same type might have
multiple orderings). I'd recommend making the DecTotalOrder argument
explicit and then providing it for your recursive case in cons.

Hope this helps,
Dan

On Mon, Oct 8, 2012 at 2:56 PM, Serge D. Mechveliani <mechvel at botik.ru>wrote:

> People,
> I have a beginner question about a  generic ordered list  definition.
>
> First, I write a special definition for  List Nat
> (for this letter I rename the math symbols
>                  \bn to Nat,  \<= to <=,  \:: to ::,  \sqcup to max
> ):
>
>   data OrderedNatList? : List Nat -> Set
>     where
>     nil    : OrderedNatList? []
>     single : (x : Nat) -> OrderedNatList? (x :: [])
>     cons   : (x y : Nat) -> (xs : List Nat) -> x <= y ->
>              OrderedNatList? (y :: xs) -> OrderedNatList? (x :: y :: xs)
>
> This is a definition of what is an  ordered list of Nat elements.
> I believe it looks natural. And it does work in my program.
>
> Then, I try to generalize it from  Nat  to  DecTotalOrder
> (this uses the  DecTotalOrder record  of  Standard Library).
> After many attempts I have wrtitten the following code which part
> before `cons' is type-checked.
>
>   open DecTotalOrder
>
>   data OrderedList? {c l1 l2 : Level} {ord : DecTotalOrder c l1 l2} :
>                     List (Carrier ord) -> Set (suc (max c (max l1 l2)))
>        where
>        nil    : OrderedList? []
>        single : (x : Carrier ord) -> OrderedList? (x :: [])
>        cons   : (x y : Carrier ord) -> (xs : List (Carrier ord)) ->
>                 _<=_ ord x y ->
>                 OrderedList? (y :: xs) ->
>                 OrderedList? (x :: y :: xs)
>
> About `cons', the checker reports "Unsolved metas"
> -- which is only due to the line  ``OrderedList? (y :: xs) ->''
>
> (in  Agda-2.3.0.1 + MAlonzo + lib-0.6).
>
> OrderedNatList?  uses recursion successfully,
> and a generic  OrderedList?  fails to type-check.
>
> Please, how to fix this?
>
> Thank you in advance for explanation,
>
> ------
> Sergei
> _______________________________________________
> 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/20121008/cfe9b356/attachment.html