Wednesday, 18 February 2009

Universes for discrimination proofs

I can't decide if this is trivial or not. What does this construction mean/say?

`module Universe wheredata N0 : Set wheredata Bool : Set where True : Bool False : Booldata Direction : Set where Left : Direction Right : Directiondata Eq (T : Set) : T -> T -> Set where refl : (t : T) -> Eq T t t-- Eq Set Bool Direction -> N0--  is not provable--  (techincally I would have to define Eq in Set1 but we can pretend universe polymorphism)mutual data U : Set where  n0 : U  bool : U  direction : U  eq : (A : U) -> T A -> T A -> U  pi : (A : U) -> (B : T A -> U) -> U  T : U -> Set T n0 = N0 T bool = Bool T direction = Direction T (eq A x y) = Eq (T A) x y T (pi A B) = (a : T A) -> T (B a)mutual data U1 : Set where  n0' : U1  bool' : U1  direction' : U1  eq' : (A : U1) -> T1 A -> T1 A -> U1  pi' : (A : U1) -> (B : T1 A -> U1) -> U1  u' : U1  lift : U -> U1  T1 : U1 -> Set T1 n0' = N0 T1 bool' = Bool T1 direction' = Direction T1 (eq' A x y) = Eq (T1 A) x y T1 (pi' A B) = (a : T1 A) -> T1 (B a) T1 u' = U T1 (lift A) = T AT' : U -> SetT' n0 = T n0T' bool = T boolT' direction = T n0T' (eq A x y) = T n0T' (pi A B) = T n0rew : forall {A B : U} -> Eq U A B -> T' A -> T' Brew (refl _) prf = prfdiscr : Eq U bool direction -> N0discr prf = rew prf Truecorr : T1 (pi' (eq' u' bool direction) \_ -> n0')corr = discr`

Sunday, 15 February 2009

Agda Supports Eta - Cont is a monad

Since Agda 2 now supports eta in the definitional equality, here is a celebratory proof that Cont is a monad!
`module eta wheredata _==_ {T : Set} : T -> T -> Set where refl : (x : T) -> x == xcont : Set -> Set -> Setcont a r = (a -> r) -> rreturn : forall {a r} -> a -> cont a rreturn a f = f a_>>=_ : forall {a b r} -> cont a r -> (a -> cont b r) -> cont b rm >>= k = \c -> m (\a -> k a c)cont-left-identity : forall {a b r} -> (o : a) -> (f : a -> cont b r) -> (return o >>= f) == f ocont-left-identity o f = refl (f o)cont-right-identity : forall {a r} -> (n : cont a r) -> (n >>= return) == ncont-right-identity n = refl ncont-associativity : forall {a b c r} -> (n : cont a r) -> (f : a -> cont b r) -> (g : b -> cont c r) -> ((n >>= f) >>= g) == (n >>= (\x -> (f x) >>= g))cont-associativity n f g = refl ((n >>= f) >>= g)`

Saturday, 7 February 2009

Inventing a concrete syntax

ind F : .

ind T : ;
I : T.

ind Bool : ;
true : Bool;
false : Bool.

ind N : ;
O : N;
S : NN.

ind Ord :
OO : Ord;
OS : OrdOrd;
OL : (NOrd) → Ord.

ind Fin : N;
fz : (n:N)Fin (S n);
fs : (n:N)Fin nFin (S n).

ind Eq (A:)(x:A):A;
refl : Eq A x x.

ind JMEq (A:)(x:A):(B:)B;
JMrefl : JMEq A x A x.

ind So : Bool;
oh : So true.

ind Ex (T:)(P:T):;
witness : (t : T)Prf(P t) → Ex T P.

ind Acc (A:)(R:AA):A;
below : ((y:A)R y xAcc A R y) → Acc A R x.

ind W (A:)(B:A):;
sup : (a:A)(f:B aW A B)W A B.

Sunday, 1 February 2009

CPS transformation using delimited continuations

`;; Idea: Use reified continuations to implement a CPS converter;;;; in the expression: (+ (* x x) (* y y));; the continuation of (* x x) is (lambda (x-squared) (+ x-squared (* y y)));;;; similiarly,;;;; in the expression: (list '+ (list '* 'x 'x) (list '* 'y 'y));; the continuation of (list '* 'x 'x) is (lambda (x-squared) (list '+ x-squared (list '* 'y 'y)))(require scheme/control) ;; shift/reset delimited continuations;; > (reset (list '+ (shift k (list '* 'x 'x))     (list '* 'y 'y)));; (* x x);; > (reset (list '+ (shift k (k '?))              (list '* 'y 'y)));; (+ ? (* y y));; > (reset (list '+ (shift k (k (list '* 'x 'x))) (list '* 'y 'y)));; (+ (* x x) (* y y));; > (reset (list '+ (shift k `(let ((x-squared ,(list '* 'x 'x))) ,(k 'x-squared))) (list '* 'y 'y)));; (let ((x-squared (* x x))) (+ x-squared (* y y)));; CPS applications should throw the result value into a continuation;; so (f x y z) turns into (f x y z (lambda (result) (continuation result)))(define (apply# f . args) (shift k (let ((g (gensym "g"))) (reset `(,f ,@args (lambda (,g) ,(k g)))))));; Some examples of apply# in action:;;;; > `(k ,(apply# 'f--> 'x 'y 'z));; (f--> x y z (lambda (g349) (k g349)));; > (apply# 'f--> (apply# '+--> 2 3) 'y 'z);; (+--> 2 3 (lambda (g345) (f--> g345 y z (lambda (g346) g346))));; > (apply# 'f--> (apply# '+--> 2 3) (apply# '*--> 'x 'y) 'z);; (+--> 2 3 (lambda (g415) (*--> x y (lambda (g416) (f--> g415 g416 z (lambda (g417) g417))))));; What about syntax like IF? clearly apply# would be wrong (due to evaluation order) so define new syntax!(define-syntax if#  (syntax-rules ()    ((if# <cond> <then> <else>) (shift k `(if ,<cond> ,(reset (k <then>)) ,(reset (k <else>)))))));; Examples:;;;; > (if# (apply# 'zero?--> 'n) ''yes ''no);; (zero?--> n (lambda (g374) (if g374 'yes 'no)));; > `(display ,(if# (apply# 'zero?--> 'n) ''yes ''no));; (zero?--> n (lambda (g850) (if g850 (display 'yes) (display 'no))))(define-syntax define#  (syntax-rules ()    ((define# (name/args ...) body) `(define (name/args ... k-->) ,(reset `(k--> ,body))))));; That's enough now to CPS convert entire procedures:;; > (define# (fact-iter--> n acc);;     (if# (apply# 'zero?--> 'n);;          'acc;;          (apply# 'fact-iter--> (apply# '---> 'n 1) (apply# '*--> 'acc 'n))))(define (fact-iter--> n acc k-->)  (zero?--> n (lambda (g875)   (if g875       (k--> acc)       (---> n 1 (lambda (g876)        (*--> acc n (lambda (g877)         (fact-iter--> g876 g877 (lambda (g878) (k--> g878)))))))))));; Test it! (this CPS format is a subset of Scheme)(define (zero?--> n k) (k (zero? n)))(define (*--> x y k) (k (* x y)))(define (---> x y k) (k (- x y)));; > (fact-iter--> 7 1 display);; 5040;; Now a function to CPS convert based on all this is trivial, it's just a fold;; that replaces if with if#, define with define# and applications with apply#!(define (if#-thunked cond then-thunk else-thunk) (if# cond (then-thunk) (else-thunk)))(define (define#-thunked name/args body-thunk)  (let ((k--> (gensym "k-->"))) `(define (,@name/args ,k-->) ,(reset `(,k--> ,(body-thunk))))))(define (cps term)  (if (pair? term)      (case (car term)        ((quote) `',term)        ((if) (if#-thunked (cps (cadr term)) (lambda () (cps (caddr term))) (lambda () (cps (cadddr term)))))        ((define) (define#-thunked (cadr term) (lambda () (cps (caddr term)))))        (else (apply apply# (map cps term))))      term));; > (cps '(define (fact-iter-2 n acc) (if (zero? n) acc (fact-iter-2 (- n 1) (* n acc)))))(define (fact-iter-2--> n acc k-->)  (zero?--> n (lambda (g443)   (if g443       (k--> acc)       (---> n 1 (lambda (g444)        (*--> n acc (lambda (g445)         (fact-iter-2--> g444 g445 (lambda (g446)          (k--> g446)))))))))));; > (fact-iter-2--> 8 1 display);; 40320`