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 where

data _==_ {T : Set} : T -> T -> Set where refl : (x : T) -> x == x

cont : Set -> Set -> Set
cont a r = (a -> r) -> r

return : forall {a r} -> a -> cont a r
return a f = f a

_>>=_ : forall {a b r} -> cont a r -> (a -> cont b r) -> cont b r
m >>= 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 o
cont-left-identity o f = refl (f o)

cont-right-identity : forall {a r} -> (n : cont a r) ->
 (n >>= return) == n
cont-right-identity n = refl n

cont-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)

Inventing a concrete syntax

ind F : ★.

ind T : ★;
I : T.

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

ind N : ★;
O : N;
S : N → N.

ind Ord : ★
OO : Ord;
OS : Ord → Ord;
OL : (N → Ord) → Ord.

ind Fin : N → ★;
fz : (n:N)Fin (S n);
fs : (n:N)Fin n → Fin (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:A → A → ★):A → ★;
below : ((y:A)R y x → Acc A R y) → Acc A R x.

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

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

alternative beta-eta equality test

import Prelude hiding (lookup,($))
import Control.Monad

type Ref = Integer

data V
 = Neutral N
 | Lam (V -> V)
 | Pi V (V -> V)
 | Set
 | Type

data N
 = App N V
 | Var Ref

Neutral n $ x = Neutral (App n x)
Lam f $ x = f x

lookup ((i, tau) : gamma) j
 | i == j = Just tau
 | otherwise = lookup gamma j
lookup [] _ = Nothing

eq gamma i f g (Pi tau sigmaF) = eq ((i, tau) : gamma) (i+1) (f $ x) (g $ x) (sigmaF x) where x = Neutral (Var i)
eq gamma i (Neutral n) (Neutral m) Set = maybe False (const True) (eqN gamma i n m)
eq gamma i s t Type = eqT gamma i s t

eqT gamma i (Pi s tF) (Pi u vF) = eqT gamma i s u && eqT ((i, s) : gamma) (i+1) (tF x) (vF x) where x = Neutral (Var i)
eqT gamma i Set Set = True

eqN gamma i (App n x) (App m y) = do
 Pi tau sigmaF <- eqN gamma i n m
 guard (eq gamma i x y tau)
 return (sigmaF x)
eqN gamma _ (Var i) (Var j)
 | i == j = lookup gamma i
 | otherwise = Nothing

-- test = eq [] 0
--   (Lam (\x -> x))
--   (Lam (\f -> Lam (\x -> f $ x)))
--   (Pi (Pi Set (\_ -> Set)) (\_ -> (Pi Set (\_ -> Set))))

-- > test
-- True

Data.Dynamic without typeclasses or unsafeCoerce

{-# LANGUAGE RankNTypes, GADTs #-}

data DYN t where
 BOOL :: DYN Bool
 INT :: DYN Integer
 (:->:) :: DYN a -> DYN b -> DYN (a -> b)

data DYNAMIC where UnDYNAMIC :: DYN t -> t -> DYNAMIC
data Equal a b where REFL :: Equal x x

mkDyn :: DYN t -> t -> DYNAMIC
mkDyn code obj = UnDYNAMIC code obj

decide :: DYN t -> DYN u -> Maybe (Equal t u)
decide BOOL BOOL = Just REFL
decide INT INT = Just REFL
decide (u :->: v) (p :->: q) = do REFL <- decide u p; REFL <- decide v q; return REFL
decide _ _ = Nothing

unbox :: DYNAMIC -> DYN t -> Maybe t
unbox (UnDYNAMIC t e) u = do REFL <- decide t u; return e

list = [ mkDyn BOOL True, mkDyn INT 34, mkDyn (BOOL :->: INT) (\x -> if x then 32 else 56) ]

-- > unbox (list !! 0) BOOL
-- Just True
-- > unbox (list !! 1) BOOL
-- Nothing
-- > unbox (list !! 2) BOOL
-- Nothing
--
-- > unbox (list !! 0) INT
-- Nothing
-- > unbox (list !! 1) INT
-- Just 34
-- > unbox (list !! 2) INT
-- Nothing
--
-- > fmap ($ True) (unbox (list !! 2) (BOOL:->:INT))
-- Just 32
-- > fmap ($ False) (unbox (list !! 2) (BOOL:->:INT))
-- Just 56
-- > fmap ($ True) (unbox (list !! 1) (BOOL:->:INT))
-- Nothing

More GADT nonsense

{-# LANGUAGE GADTs #-}

data CON f a fa k z where
 CTR :: c -> CON f a c z z
 VAR :: CON f a (a -> r) k z -> CON f a r (a -> k) z
 REC :: CON f a (f a -> r) k z -> CON f a r (f a -> k) z

infixr :+:
data SUM f a ka z where
 ZRO :: SUM f a (f a -> z) z
 (:+:) :: CON f a (f a) k z -> SUM f a ka z -> SUM f a (k -> ka) z


size :: kase -> SUM f a kase Integer -> f a -> Integer
size kase code = size' kase code kase code
size' :: kase -> SUM f a kase Integer -> ka -> SUM f a ka Integer -> f a -> Integer
size' kase code ka ZRO = ka
size' kase code ka (t :+: ts) = size' kase code (ka (sizeCON kase code 0 t)) ts
sizeCON :: kase -> SUM f a kase Integer -> Integer -> CON f a i0 k Integer -> k
sizeCON kase code k (CTR _) = 0 + k
sizeCON kase code k (VAR r) = \_ -> sizeCON kase code (1 + k) r
sizeCON kase code k (REC r) = \x -> sizeCON kase code (size kase code x + k) r


dfs :: kase -> SUM f a kase [a] -> f a -> [a]
dfs kase code = dfs' kase code kase code
dfs' :: kase -> SUM f a kase [a] -> ka -> SUM f a ka [a] -> f a -> [a]
dfs' kase code ka ZRO = ka
dfs' kase code ka (t :+: ts) = dfs' kase code (ka (dfsCON kase code [] t)) ts
dfsCON :: kase -> SUM f a kase [a] -> [a] -> CON f a i0 k [a] -> k
dfsCON kase code k (CTR _) = k
dfsCON kase code k (VAR r) = \a -> dfsCON kase code (a : k) r
dfsCON kase code k (REC r) = \x -> dfsCON kase code (dfs kase code x ++ k) r


data Both a = a :&: a
(&) = VAR (VAR (CTR (:&:)))
both = (&) :+: ZRO
bothCase (&) (x :&: y) = x & y
bothCaseR (&) (x :&: y) = y & x

data List a = Nil | Cons a (List a)
nil = CTR (Nil)
cons = REC (VAR (CTR (Cons)))
list = nil :+: cons :+: ZRO
listCase nil cons Nil = nil
listCase nil cons (Cons x xs) = cons x xs
listCaseR nil cons Nil = nil
listCaseR nil cons (Cons x xs) = cons xs x

data Tree a = Leaf a | Branch (Tree a) (Tree a)
leaf = VAR (CTR (Leaf))
branch = REC (REC (CTR Branch))
tree = leaf :+: branch :+: ZRO
treeCase leaf branch (Leaf a) = leaf a
treeCase leaf branch (Branch l r) = branch l r
treeCaseR leaf branch (Leaf a) = leaf a
treeCaseR leaf branch (Branch l r) = branch r l

-- > size bothCaseR both (True :&: False)
-- 2
-- > size listCaseR list (Cons 'x' (Cons 'y' (Cons 'z' Nil)))
-- 3
-- > size treeCaseR tree (Branch (Leaf ()) (Branch (Branch (Leaf ()) (Leaf ())) (Leaf ())))
-- 4
-- > dfs listCaseR list (Cons 'x' (Cons 'y' (Cons 'z' Nil)))
-- "xyz"
-- > dfs treeCaseR tree (Branch (Leaf 4) (Branch (Branch (Leaf 3) (Leaf 5)) (Leaf 7)))
-- [4,3,5,7]

beta eta equality for STLC by NbE

{-# LANGUAGE NoMonomorphismRestriction #-}

import Prelude hiding (($))
import Control.Monad

type Ref = Int
newtype Scope a = Scope a deriving (Eq, Show)
data T = O | T :->: T deriving (Eq, Show)
data S = Var Ref | Lam T (Scope S) | App S S
       | Quote Ref deriving (Eq, Show)

abstract i t = Scope (extract 0 t) where
 extract r (Var j) = Var j
 extract r (Lam t (Scope b)) = Lam t (Scope (extract (r+1) b))
 extract r (App m n) = App (extract r m) (extract r n)
 extract r (Quote j)
  | j == i = Var r
  | otherwise = Quote j

gamma |- Var i = Just (gamma !! i)
gamma |- Lam u (Scope b) = do v <- (u:gamma) |- b ; return (u :->: v)
gamma |- App m n = do u :->: v <- gamma |- m ; u' <- gamma |- n ; guard (u == u') ; return v

data V = VLam (V -> V)
       | VNeutral N
data N = NApp N V
       | NQuote Ref

VLam f $ x = f x
VNeutral n $ x = VNeutral (NApp n x)

eval delta (Var j) = delta !! j
eval delta (Lam _ (Scope b)) = VLam (\x -> eval (x:delta) b)
eval delta (App m n) = eval delta m $ eval delta n

------------------- OLD
-- r :: T -> V -> V
-- r O e = e
-- r (tau :->: sigma) f = VLam (\x -> r sigma (f $ (r tau x)))

------------------- NEW
r :: T -> V -> V
r O e = e
r (tau :->: sigma) f = f $ VLam (\f -> r sigma (VLam (\x -> f $ (r tau x))))



q i (VLam f) = Lam O (abstract i (q (i+1) (f (VNeutral (NQuote i)))))
q i (VNeutral n) = nq i n

nq i (NApp m n) = App (nq i m) (q i n)
nq i (NQuote j) = Quote j

nf tm = fmap (q 0 . flip r (eval [] tm)) ([] |- tm)

identity = Lam (O :->: O) (Scope (Var 0))
dollar = Lam (O :->: O) (Scope (Lam O (Scope (App (Var 1) (Var 0)))))


{- OLDER
{-# LANGUAGE NoMonomorphismRestriction #-}

import Control.Monad

type Ref = Int
newtype Scope a = Scope a deriving (Eq, Show)
data T = O | T :->: T deriving (Eq, Show)
data S = Var Ref | Lam T (Scope S) | App S S
       | Quote Ref deriving (Eq, Show)

gamma |- Var i = Just (gamma !! i)
gamma |- Lam u (Scope b) = do v <- (u:gamma) |- b ; return (u :->: v)
gamma |- App m n = do u :->: v <- gamma |- m ; u' <- gamma |- n ; guard (u == u') ; return v

data V = VLam T (V -> V) | VNeutral N
       | VQuote Ref
data N = NVar V | NApp N V
       | NQuote Ref

lift i (Var j)
 | j < i = Var j
 | otherwise = Var (j+1)
lift i (Lam t (Scope b)) = Lam t (Scope (lift (i+1) b))
lift i (App m n) = App (lift i m) (lift i n)

abstract i t = Scope (extract 0 t) where
 extract r (Var j) = Var j
 extract r (Lam t (Scope b)) = Lam t (Scope (extract (r+1) b))
 extract r (App m n) = App (extract r m) (extract r n)
 extract r (Quote j)
  | j == i = Var r
  | otherwise = Quote j

eta u t = Lam u (Scope (App (lift 0 t) (Var 0)))

etaReify (u :->: v) (Lam t (Scope b)) delta gamma = VLam u (\x -> etaReify v b (x:delta) (u:gamma))
etaReify (u :->: v) t delta gamma = etaReify (u :->: v) (eta u t) delta gamma
etaReify O t delta gamma = betaEtaReify O t delta gamma

betaEtaReify _   (Var i) delta gamma = delta !! i
betaEtaReify tau (Lam t (Scope b)) delta gamma = etaReify tau (Lam t (Scope b)) delta gamma
betaEtaReify tau (App m n) delta gamma = app (betaEtaReify (sigma :->: tau) m delta gamma) (etaReify sigma n delta gamma)
 where sigma = case gamma |- n of Nothing -> error "Type error" ; Just sigma -> sigma
       app (VLam _ f) x = f x
       app (VNeutral n) x = VNeutral (NApp n x)
       app (VQuote j) x = VNeutral (NApp (NQuote j) x)

quote i (VLam t f) = Lam t (abstract i (quote (i+1) (f (VQuote i))))
quote i (VNeutral n) = nquote i n
quote i (VQuote j) = Quote j

nquote i (NVar v) = quote i v
nquote i (NApp n v) = App (nquote i n) (quote i v)
nquote i (NQuote j) = Quote j

betaEtaNF p = do
 t <- [] |- p
 return (quote 0 (etaReify t p [] []))

betaEtaEqual p q = do
 t <- [] |- p ; t' <- [] |- q ; guard (t == t')
 return (quote 0 (etaReify t p [] []) == quote 0 (etaReify t q [] []))

identity = Lam (O :->: O) (Scope (Var 0))
dollar = Lam (O :->: O) (Scope (Lam O (Scope (App (Var 1) (Var 0)))))

-- > betaEtaEqual identity dollar
-- Just True
-}