PasteRack.org
Paste # 40712
2019-12-07 10:03:13

Fork as a new paste.

Paste viewed 541 times.


Embed:

Y in Typed/Racket

  1. #lang typed/racket/base
  2.  
  3. ( : R (∀ (α) (-> (Rec t (-> t α)) α)) )
  4. (define (R f)
  5.   (f f))
  6.  
  7. ((inst R (-> (Listof Any) Exact-Nonnegative-Integer))
  8.  (λ (length)
  9.    (λ (l)
  10.      (cond [(null? l) 0]
  11.            [else (add1 ((length length)
  12.                         (cdr l)))]))))
  13.  
  14. ( : make-length (-> (Rec t (-> t (-> (Listof Any) Exact-Nonnegative-Integer)))
  15.                     (-> (Listof Any) Exact-Nonnegative-Integer)))
  16. (define ((make-length length) lst)
  17.   (cond
  18.     [(null? lst) 0]
  19.     [else (add1 ((length length) (cdr lst)))]))
  20.  
  21. ((R make-length)
  22.  '(a b c d))
  23.  
  24. ( : Y
  25.     (∀ (α β)
  26.        (-> (-> (-> α β) (-> α β))
  27.            (-> α β))) )
  28. (define (Y b)
  29.   ((ann (λ (f) (b (λ (x) ((f f) x))))
  30.         (-> (Rec t (-> t (-> α β)))
  31.             (-> α β)))
  32.    (λ (f) (b (λ (x) ((f f) x))))))
  33.  
  34. (define len
  35.   ((inst Y (Listof Any) Exact-Nonnegative-Integer)
  36.    (λ (length)
  37.      (λ (l)
  38.        (cond [(null? l) 0]
  39.              [else (add1 (length (cdr l)))])))))
  40.  
  41. (len '(1 2))
  42.  
  43. (len '(A B D E F G H))

=>

- : (-> (Listof Any) Nonnegative-Integer)

#<procedure>

- : Integer [more precisely: Nonnegative-Integer]

4

- : Integer [more precisely: Nonnegative-Integer]

2

- : Integer [more precisely: Nonnegative-Integer]

7