[racket] typed racket cps, state machines

1. Your programs don't look like conventional cps. Perhaps you're thinking 2-way continuations (as in Prolog implementations). 

2. Don't use polymorphism. Just use (define (halt) (printf "done") (halt)) as the proper halt continuation, often falsely called initial continuation. 

3. Think about the algorithm. This hint comes in the form of a cps algorithm: 

  http://pasterack.org/pastes/55294

#lang typed/racket

(require typed/rackunit)

(define-type Λ               ;; e = (is one of)
  (U Symbol                  ;; x
     (List 'lambda Symbol Λ) ;; λx.e
     (List Λ Λ)              ;; (e e)
     ))

(: e1 Λ)
(define e1 'x)

(: e2 Λ)
(define e2 '(lambda x x))

(: e3 Λ)
(define e3 `(,e1 ,e2))

(: e1-cps Λ)
(define e1-cps '(lambda k (k x)))

(: e2-cps Λ)
(define e2-cps '(lambda k (k (lambda x (lambda k (k x))))))

(: e3-cps Λ)
(define e3-cps `(lambda k (,e1-cps (lambda k-e1 (,e2-cps (lambda k-e2 ((k-e1 k-e2) k)))))))

(: cps (-> Λ Symbol Λ))

(define (cps e k)
  (match e 
    [(? symbol? x) `(lambda ,k (,k ,x))]
    [`(lambda ,(? symbol? x) ,e) `(lambda ,k (,k (lambda ,x ,(cps e 'k))))]
    [`(,f ,a) `(lambda ,k (,(cps f 'k) (lambda k-e1 (,(cps a 'k) (lambda k-e2 ((k-e1 k-e2) ,k))))))]))

(check-equal? (cps e1 'k) e1-cps)
(check-equal? (cps e2 'k) e2-cps)
(check-equal? (cps e3 'k) e3-cps)

;; ---------------------------------------------------------------------------------------------------
;; now write an evaluator for Λ and run the examples 

(: halt Λ)
(define halt '(lambda x x))

(: e1-run-cps Λ)
(define e1-run-cps `(,e1 ,halt))

(: e2-run-cps Λ)
(define e2-run-cps `(,e2 ,halt))

(: e3-run-cps Λ)
(define e3-run-cps `(,e3 ,halt))




On Sep 5, 2014, at 11:12 AM, Anthony Carrico <acarrico at memebeam.org> wrote:

> Thanks for occasional help learning typed racket on IRC. I'm still
> finding the pitfalls that await those of us used to dynamically typed
> programs.
> 
> The other day I posted some cps patterns I figured out:
>  http://pasterack.org/pastes/49759
> 
> Extending that to simple state machines that loop through various states
> gets me into trouble. The simplest example is just looping through one
> state, or not:
> 
> (define #:∀ (B0V B1V)
>  (p0 (branch0 : (-> B0V))
>      (branch1 : (-> B1V)))
>  : (U B0V B1V)
> 
>  ;; This one is fine:
>  (define (no-loop) : (U B0V B1V)
>    (branch0))
> 
>  ;; insufficient type information to typecheck this one:
>  (define (loop) : (U B0V B1V)
>    (loop))
> 
>  ;; insufficient type information to typecheck this one too:
>  (define (loop*) : (U B0V B1V)
>    ((inst loop* B0V B1V)))
> 
>  ;; insufficient type information to typecheck this one too:
>  (define (loop**) : (U B0V B1V)
>    ((inst loop** (U B0V B1V) (U B0V B1V))))
> 
>  (no-loop)
>  (loop)
>  (loop*)
>  (loop**))
> 
> I'm still thinking about this problem, but since I have distilled it to
> the simplest cases, I thought I'd post. I have the intuition that this
> has something to do with the nested instantiation of polymorphic types.
> The unions would "obviously" (to a human) collapse, but I suppose the
> type checker isn't picking up on this.
> 
> -- 
> Anthony Carrico
> 
> ____________________
>  Racket Users list:
>  http://lists.racket-lang.org/users