0. #lang racket
1.  
2. (require (prefix-in racket: racket))
3. (require syntax/parse/define)
4.  
5. (define-syntax-parser TODO
6.   [_ #'(error "TODO: unimplemented")])
7.  
8. (define-signature cat^ (identity compose))
9. (define-signature products^ (pi1 pi2 pair into-terminal))
10. (define-signature sums^ (in1 in2 split from-initial))
11. (define-signature exponentials^ (lambda eval))
12.  
13. (define-signature contexts^
14.   (context-empty  ;; ctx
15.    context-get    ;; ctx, sym -> Γ → A
16.    context-extend ;; ctx, sym -> ctx, (Γ × A → Γ,A)
17.    ))
18.  
19. (define-unit racket@
20.   (import)
21.   (export cat^ products^ sums^ exponentials^)
22.   (define identity racket:identity)
23.   (define compose racket:compose1)
24.   (define pi1 car)
25.   (define pi2 cdr)
26.   (define ((pair f g) x) (cons (f x) (g x)))
27.   (define (into-terminal x) '())
28.   (define (in1 x) `(left ,x))
29.   (define (in2 x) `(rght ,x))
30.   (define ((split f g) x)
31.     (match x [`(left ,y) (f y)] [`(rght ,y) (g y)]))
32.   (define (from-initial _) (error "impossible"))
33.   (define (eval x) ((car x) (cdr x)))
34.   (define (((lambda f) a) b) (f (cons a b)))
35.   )
36.  
37. (define-unit products->contexts@
38.   (import cat^ products^)
39.   (export contexts^)
40.   (define context-empty '())
41.   (define (context-get ctx sym)
42.     (match ctx
43.       ['() (error "unbound symbol")]
44.       [(cons (== sym) _) pi2]
45.       [(cons _ xs) (compose pi1 (context-get xs sym))]))
46.   (define (context-extend ctx sym)
47.     (values (cons sym ctx) identity)))
48.  
49. (define-compound-unit/infer racket+contexts@
50.   (import)
51.   ;; ugh, look at all this boilerplate.
52.   (export cat^ products^ sums^ exponentials^ contexts^)
53.   (link racket@ products->contexts@))
54.  
55. 
56. ;; ---------- SIMPLY TYPED λ-CALCULUS ----------
57. (define-signature stlc^
58.   (var     ;; x -> (Γ → A)      where x:A ∈ Γ
59.    lambda  ;; x, (Γ,x:A → B) -> (Γ → A => B)
60.    apply   ;; (Γ → A => B), (Γ → A) -> (Γ → B)
61.    project ;; i, n, (Γ → Πᵢⁿ Aᵢ) -> (Γ → Aᵢ)
62.    tuple   ;; (Γ → Aᵢ)ᵢⁿ -> (Γ → Πᵢⁿ Aᵢ)
63.    ))
64.  
65. (define-unit cat->stlc@
66.   (import cat^ contexts^ products^ (prefix exp: exponentials^))
67.   (export stlc^)
68.   ;; our Γ → A is represented as (ctx -> (Γ → A))
69.   (define ((var name) ctx) (context-get ctx name))
70.   (define ((apply e1 e2) ctx) (compose (pair (e1 ctx) (e2 ctx)) exp:eval))
71.   (define ((lambda x e) ctx)
72.     (define-values (e-ctx extend-morph) (context-extend ctx x))
73.     ;; exp:lambda : (Γ × A → B) -> (Γ → A => B)
74.     (exp:lambda (compose (e e-ctx) extend-morph)))
75.   (define ((project i n e) ctx)
76.     (match n
77.       [0 (compose into-terminal (e ctx))]
78.       [1 (e ctx)]
79.       [2 (compose (match i [0 pi1] [1 pi2]) (e ctx))]
80.       [_ TODO]))
81.   (define ((tuple . es) ctx)
82.     (match es
83.       [`() TODO]
84.       [`(,e) TODO]
85.       [`(,e1 ,e2) TODO]
86.       [_ TODO])))
87.  
88. (define-compound-unit/infer racket-stlc@
89.   (import)
90.   (export stlc^ contexts^)
91.   (link racket+contexts@ cat->stlc@))
92.  
93. 
94. (module+ test
95.   (require rackunit)
96.   (define-values/invoke-unit/infer racket-stlc@)
97.   (check-eqv? 2 ((((lambda 'x (var 'x)) context-empty) 'ignored) 2))
98.   )

=>