writing a dependent type in agda to guarantee a list is sorted

Question

I have a record type, call if Foo, in Agda. I can sort it by generating a String representation (display foo) and sorting the resulting strings. I have a relation, call it <=Foo, for comparing Foo records which has one constructor, $<=Foo$, that takes evidence ((display a) Data.String.Base.<= (display b)) that the string for a is LT the string for b. I've proven it's a DecTotalOrder, yielding fooTotalOrder

I would now like to make a dependent type that enforces that a list is in sorted order. It seems this should be

Σ[ l ∈ (List Foo) ] (FooSorted.Sorted l)

where FooSorted.Sorted comes from passing fooTotalOrder to Data.List.Relation.Unary.Sorted.TotalOrder.

As I understand, to make this work, I need a function, say

fooSorted : (l : List Foo) -> (FooSorted.Sorted l)

FooSorted is derived from Data.List.Relation.Unary.Linked.Linked which is defined as

data Linked (R : Rel A ℓ) : List A → Set (a ⊔ ℓ) where
    []  : Linked R []
    [-] : ∀ {x} → Linked R (x ∷ [])
    _∷_ : ∀ {x y xs} → R x y → Linked R (y ∷ xs) → Linked R (x ∷ y ∷ xs)

Here, R is <=Foo.

It seems to me that fooSorted needs to return Linked <=Foo l where l is the List Foo argument.

The first two cases are straightforward, but I cannot figure out the last one. I need to use evidence that (x <=Foo y). I have the constructor for that, but it requires evidence that ((display x) Data.String.Base.≤ (display x)) and I do not see where to get that.

I cannot simply enter that - it won't compile. From the various ways I can get back a similar type, the closest is using total order, but that returns a sum type and I don't see how to get just the one value from it.

The example I'm trying to imitate, using isEven, won't compile if an odd number is used where an even is needed. I'm looking for the same for lists - the program should not compile if a list is not sorted - but I do want my dependent type to compile.

It's entirely possible I've headed in completely the wrong direction. Any help is appreciated!

The closest I have come is the following:

fooSorted (x ∷ x₁ ∷ m) =  Linked.∷ ($<=Foo$ (getProof x x₁)) (rectype (x₁ ∷ m))
   where
      getProof : (a : Foo) → (b : Foo) → ((display a) Data.String.Base.≤ (display b))
      getProof a b with decLT (display a) (display b)
      ...      | yes P = P
      ...      | no Q = {!  !}

The P in the yes branch is exactly what I want, but what to put in the other hole? The intent is that the proof fails.

Answer 1

Thank you for the suggestions, and sorry for the delay with a response. In the end I wasn't able to take advantage of the approach Naïm suggested, which would have worked for strictly static instances. In the end I needed to follow the last suggestion - which essentially involved reinventing bubble sort. This way I would eventually end up with the item at the start of the list (let's say a) and use the second constructor from Linked.

Then I would have the next one (say b) of the list and check that b <= a getting b :: a :: [], or create a new list a :: b :: [].

Then as each additional item was added I could check it against its predecessor before adding to the list or recursively sorting its way into the existing list. So, if given a sorted list, this returns a dependently typed sorted list in O(n) time, and otherwise can be O(n^2)

Fortunately, once a list is sorted, all the other operations I wanted to do maintain order.