[racket] Typed Inference Assistance

From: Ray Racine (ray.racine at gmail.com)
Date: Fri Jul 20 11:11:50 EDT 2012

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)))
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20120720/5db1a61c/attachment.html>

Posted on the users mailing list.