[TYPES] An efficient program for the function (mod 3) in type theories

[Conor McBride]

Hi Yong

Yong Luo wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Dear all,
>
> I am looking for an efficient program of the following function in the
> Martin-Lof's type theory or UTT.
>   

As well you know, I wrote a program which will spit out the program you 
want, given (more or less) the program you've written.

> f :: Nat -> Nat
>
> f (zero) = zero
> f (succ(zero)) = succ(zero)
> f (succ(succ(zero))) =  succ(succ(zero))
> f (succ(succ(succ(x)))) = f (x)
>   

> In the Martin-Lof's type theory or UTT, every function is defined by
> eliminators of inductive data types. I would like to know whether it is
> possible to have an efficient program for the function f.
>   

Yes it is. The pattern matching equations hold computationally for the 
UTT programs which the translation spits out. Given a suitable reduction 
strategy (ie, one designed to exploit this property of the translation), 
you get a constant factor blowup in the number of steps, ie a larger 
number of smaller steps.

Hope this helps

Conor