quick sort in a total language. We use a Nat-like type to track the maximum number of steps, and show that we are always decreasing on the size of the list. This is a general strategy: compute first an upper bound of some kind using a Nat, then recurse carrying that counter through as proof that we will terminate.

sort.bosatsu

# use this to track the maximum size of a list    
enum Size: Z, S(prev: Size)    
    
def size(list, acc):    
    recur list:    
        []: acc    
        [_, *t]: size(t, S(acc))    
    
def sort(ord: Order[a], list: List[a]) -> List[a]:    
    Order { to_Fn } = ord    
    
    def loop(list: List[a], sz: Size):    
        recur sz:    
            Z: list    
            S(n):    
                match list:    
                    []: []    
                    [h, *t]:    
                        def lt(x): match to_Fn(x, h):    
                                     LT: True    
                                     _: False    
                        def gt(x): match to_Fn(x, h):    
                                     GT: True    
                                     _: False    
                        lesser = [ ta for ta in t if lt(ta) ]    
                        greater = [ ta for ta in t if gt(ta) ]    
                        # each of the above are at most size n    
                        [ *loop(lesser, n), h, *loop(greater, n) ]    
    loop(list, size(list, Z))