[Agda] generic type recursion

[Serge D. Mechveliani]

On Mon, Oct 08, 2012 at 03:03:50PM -0400, Daniel Peebles wrote:
> 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.

Great! This type-checks. Thank you.
Initially, this argument   (ord : DecTotalOrder c l1 l2)  
was explicit. But the checker reported of a wrongly used indices in 
`cons'. And I did various changes, including hiding of  ord.
Now, I return to explicit  (ord : DecTotalOrder c l1 l2),   and it type-
checks.

It is difficult to believe that such a complex type system as of Agda
can be practically implemented.

Regards,
Sergei.


> On Mon, Oct 8, 2012 at 2:56 PM, Serge D. Mechveliani <mechvel at botik.ru>wrote:
[..]
> > 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)
[..]