In the below "head" procedure, [(Datum d) (Done 'EOS d)] does not type
check. I'm not sure how I inform the type checker to just "lift" d to type
(Option D).
#lang typed/racket/base
(require racket/match)
;; Input stream of datum D
(define-type (Stream D) (U (Datum D) 'Nothing 'EOS))
(struct: (D) Datum ([iota : D]))
;; Iteratee
(define-type (Iteratee D A) (U (Done D A) (Continuation D A)))
(struct: (D A) Done ([stream : (Stream D)] [accum : A]))
(struct: (D A) Continuation
([resume : ((Stream D) -> (U (Done D A) (Continuation D A)))])) ;; ... ->
(Iteratee D A)
(: run (All (D A) (Iteratee D A) -> A))
(define (run iter)
(match iter
[(Done _ accum) accum]
[(Continuation resume) (run (resume 'EOS))]))
(: iterator (All (D A) (Listof D) (Iteratee D A) -> (Iteratee D A)))
(define (iterator lst iter)
(match (cons lst iter)
[(cons '() i) i]
[(cons _ (Done _ _)) iter]
[(cons (list-rest x xs) (Continuation k)) (iterator xs (k (Datum x)))]))
(: counter (All (D) (-> (Iteratee D Integer))))
(define (counter)
(: step (Integer -> ((Stream D) -> (Iteratee D Integer))))
(define (step n)
(λ: ((str : (Stream D)))
(match str
[(Datum _) (Continuation (step (add1 n)))]
['Nothing (Continuation (step n))]
['EOS (Done 'EOS n)])))
(Continuation (step 0)))
;; e.g. (run (iterator '(1 2 3) ((inst counter Integer))))
(: drop (All (D) Integer -> (Iteratee D Void)))
(define (drop n)
(: step (-> ((Stream D) -> (Iteratee D Void))))
(define (step)
(λ: ((str : (Stream D)))
(match str
[(Datum _) (drop (sub1 n))]
['Nothing (Continuation (step))]
['EOS (Done 'EOS (void))])))
(if (zero? n)
(Done 'Nothing (void))
(Continuation (step))))
(: head (All (D) (-> (Iteratee D (Option D)))))
(define (head)
(: step (-> ((Stream D) -> (Iteratee D (Option D)))))
(define (step)
(λ: ((str : (Stream D)))
(match str
[(Datum d) (Done 'EOS d)]
['Nothing (Continuation (step))]
['EOS (Done 'EOS #f)])))
(Continuation (step)))
____________________
Racket Users list:
http://lists.racket-lang.org/users
