[Agda] size-based termination

[Andreas Abel]

On 12/21/10 6:12 PM, Conor McBride wrote:
> You may find Andreas Abel's "sized types" useful in this respect. Agda does
> have an experimental implementation of them, doesn't it?

There is an implementation that works in some cases.  I must admit that 
I cannot promise more at the moment (debugging required...).

Attached is the notorious quicksort example.  As you can see in the 
"Trash" section, my original algorithm with "with" does not pass the 
type checker due to bad interaction of sized-types features and with.

The CPS version of partition works fine...

> Alternatively, you might index your datatype by a size (or an upper bound
> on size). If the size decreases structurally, you're sorted.
>
> Explicit size indexing can be a nuisance without some cheap means to
> inflate the bound: that's a big part of what "sized types" sort out.
>
> It's certainly worth looking in that direction.
>
> I see Andreas has just suggested the "gasoline" method...
;-)

Cheers,
Andreas
-------------- next part --------------
{-# OPTIONS --sized-types #-}

module Quicksort where

open import Size


-- Booleans

data Bool : Set where
  true false : Bool

if_then_else_ : {A : Set} -> Bool -> A -> A -> A
if true  then a else b = a
if false then a else b = b

-- Lists

infixr 4 _::_

data List (A : Set) : {i : Size} -> Set where
  []   : {i : Size} -> List A {↑ i}
  _::_ : {i : Size} -> A -> List A {i} -> List A {↑ i}

-- Partition 

partition : {A : Set} -> (A -> Bool) -> {i : Size} -> List A {i} -> 
            {C : Set} -> (List A {i} -> List A {i} -> C) -> C
partition p []        k = k [] []
partition p (a :: as) k = partition p as \ l r ->
  if p a then k (a :: l) r else k l (a :: r)

-- Quicksort

DecRel : Set -> Set
DecRel A = A -> A -> Bool

qsapp : {A : Set} -> DecRel A -> {i : Size} -> List A {i} -> List A -> List A
qsapp _<=_ []        acc = acc
qsapp _<=_ (a :: as) acc = partition (\ x -> x <= a) as \ l r ->
  qsapp _<=_ l (a :: qsapp _<=_ r acc)

quicksort : {A : Set} -> DecRel A -> List A -> List A
quicksort _<=_ l = qsapp _<=_ l []

-- Trash

{-
partition : {A : Set} -> (A -> Bool) -> {i : Size} ->
            List A {i} -> List A {i} × List A {i}
partition p [] = [] , []
partition p (a :: as) with partition p as
... | l , r = if p a then (a :: l) , r else (l , (a :: r))
-}