;;; $Id: combinators.scm,v 1.3 2006/01/05 22:24:09 leavens Exp $
;;; AUTHOR: Gary T. Leavens
;;;
;;; Note that lots of this file cannot be type checked for fundamental reasons.
;;; Also, we don't eta-reduce several of the combinator defintions,
;;; so that this file also works in Chez Scheme.

(module combinators (lib "typedscm.ss" "typedscm")

(provide I K S B zero add1 D)

(deftype I (forall (T) (-> (T) T)))
(define I
  (lambda (x) x))

(deftype K (forall (S T) (-> (T) (-> (S) T))))
(define K
  (lambda (x)
    (lambda (y) x)))

;;; The type for S isn't as polymorphic as it should be,
;;; but the type system used here doesn't allow its true type to be expressed.
(deftype S
  (forall (S T U) (-> ((-> (T) (-> (S) U))) (-> ((-> (T) S)) (-> (T) U)))))
(define S
  (lambda (x)
    (lambda (y)
      (lambda (z)
        ((x z) (y z))))))

;; The following is the type B would have if S had the right type
(deftype B (forall (S T U) (-> ((-> (S) U)) (-> ((-> (T) S)) (-> (T) U)))))
(define B
  (lambda (x)
    (((S (K S)) K) x)))

;; The type of zero can't be inferred...
(deftype zero (forall (S T U) (-> ((-> (S) U)) (-> (T) T))))
(define zero
  (lambda (f)
    ((K I) f)))

(deftype add1
  (forall (S T U)
     (-> ((-> ((-> (S) U)) (-> (T) S))) (-> ((-> (S) U)) (-> (T) U)))))
(define add1
  (lambda (f)
    ((S B) f)))

;; the type of D can't be inferred...
(define D
  ;; EQUATIONS: (((D X) Y) zero) = X
  ;;            (((D X) Y) (add1 Z)) = Y
  (has-type-trusted
    (forall (S T U)
      (-> (S)
          (-> (U)
              (-> ((-> ((-> (T) T)) (-> (T) T)))
                  (-> ((-> (T) T)) (-> (T) T))))))
    (lambda (x)
      (lambda (y)
        (lambda (f)
          ((((S (K (S ((S (K S)) ((S (K (S I))) ((S (K K)) K))))))
             ((S (K K)) K)
             x) y) f))))))

) ;; end module