Skip to content

Commit 401f693

Browse files
dvanhorndvanhorn
committed
Start of type inference.
1 parent 22b22b3 commit 401f693

1 file changed

Lines changed: 349 additions & 0 deletions

File tree

‎www/notes/loot/type.rkt‎

Lines changed: 349 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,349 @@
1+
#lang racket
2+
3+
;; type TypeEnv = (Listof (List Variable Type))
4+
5+
;; type Type =
6+
;; | 'Bool
7+
;; | 'Int
8+
;; | `(,Type -> ,Type)
9+
;; | TVariable
10+
11+
;; type TVariable = Symbol (except 'Bool or 'Int)
12+
13+
;; type Expr =
14+
;; | Integer
15+
;; | Boolean
16+
;; | `(λ (,Variable) ,Expr)
17+
;; | `(,Expr ,Expr)
18+
19+
;; type Constraints = (Listof (List Type Type))
20+
;; Interp: a set of equality constraints between each pair of types in the list
21+
22+
23+
;; TypeEnv Expr -> (Maybe Type)
24+
(define (type-infer G e)
25+
(match (type-constraints G e)
26+
[(list t C)
27+
(maybe-apply apply-solution (unify C) t)]))
28+
29+
;; TypeEnv Expr -> (List TVariable Constraints)
30+
(define (type-constraints G e)
31+
(match e
32+
[#t '(Bool ())]
33+
[#f '(Bool ())]
34+
[(? integer?) '(Int ())]
35+
[(? symbol? x) (list (lookup x G) '())]
36+
[`(λ (,x) ,e)
37+
(let ((t1 (gensym)))
38+
(match (type-constraints (cons (list x t1) G) e)
39+
[(list t2 C)
40+
(let ((t (gensym)))
41+
(list t (append `((,t (,t1 -> ,t2))) C)))]))]
42+
[`(,e0 ,e1)
43+
(match (type-constraints G e0)
44+
[(list t0 C0)
45+
(match (type-constraints G e1)
46+
[(list t1 C1)
47+
(let ((t (gensym)))
48+
(list t (append `((,t0 (,t1 -> ,t))) C0 C1)))])])]))
49+
50+
;; Is x a type variable? (a symbol that's not 'Int or 'Bool)
51+
(define (tvariable? x)
52+
(and (symbol? x)
53+
(not (memq x '(Bool Int)))))
54+
55+
;; type Subst = (Listof (List TVariable Type))
56+
;; Invariant: no variable in lhs occurs in any term earlier in the list
57+
58+
;; Constraints -> (Maybe Subst)
59+
(define (unify C)
60+
(match C
61+
['() '()]
62+
[(cons (list T1 T2) C)
63+
(let ((s1 (unify C)))
64+
(let ((s2 (maybe-apply unify-one
65+
(maybe-apply apply-solution s1 T1)
66+
(maybe-apply apply-solution s1 T2))))
67+
(maybe-apply append s1 s2)))]))
68+
69+
;; Type Type -> (Maybe Subst)
70+
;; Generate a substitution which unifies T1 and T2 (if possible)
71+
(define (unify-one T1 T2)
72+
(if (eq? T1 T2)
73+
'()
74+
(match* (T1 T2)
75+
[(`(,T1 -> ,T2) `(,T3 -> ,T4))
76+
(unify `((,T1 ,T3) (,T2 ,T4)))]
77+
[((? tvariable? t) T)
78+
(and (not (occurs? t T))
79+
`((,t ,T)))]
80+
[(T (? tvariable? t))
81+
(and (not (occurs? t T))
82+
`((,t ,T)))]
83+
[(_ _) #f])))
84+
85+
;; TVariable Type -> Boolean
86+
;; Does t occur in T?
87+
(define (occurs? t T)
88+
(match T
89+
[(? tvariable? y) (eq? t y)]
90+
[`(,T1 -> ,T2) (or (occurs? t T1)
91+
(occurs? t T2))]
92+
[_ #f]))
93+
94+
;; X (Maybe (Listof X)) -> (Maybe (Listof X))
95+
(define (maybe-cons x mxs)
96+
(and mxs (cons x mxs)))
97+
98+
;; (X ... -> Z) (Maybe X) ... -> (Maybe Z)
99+
(define (maybe-apply f . xs)
100+
(and (andmap identity xs) (apply f xs)))
101+
102+
103+
;; Solution Type -> Type
104+
(define (apply-solution s T)
105+
(match s
106+
['() T]
107+
[(cons (list t T*) s)
108+
(apply-solution s (subst-type T* t T))]))
109+
110+
;; Type Symbol Constaints -> Contraints
111+
;; Substitute T for t in C
112+
(define (subst T t C)
113+
(map (λ (c) (map (λ (T*) (subst-type T t T*)) c))
114+
C))
115+
116+
;; Type Symbol Type -> Type
117+
;; Substitute T for t in T*
118+
(define (subst-type T t T*)
119+
(match T*
120+
['Bool 'Bool]
121+
['Int 'Int]
122+
[(? symbol? t*) (if (equal? t t*) T T*)]
123+
[`(,t1 -> ,t2)
124+
`(,(subst-type T t t1) -> ,(subst-type T t t2))]))
125+
126+
127+
128+
129+
130+
131+
132+
133+
134+
#|
135+
;; Constraints -> Boolean
136+
(define (unifiable? C)
137+
(match C
138+
['() #t]
139+
[(cons (list (? variable? t) T) C)
140+
(unifiable? (subst T t C))]
141+
[(cons (list T (? variable? t)) C)
142+
(unifiable? (subst T t C))]
143+
[(cons (list T1 T2) C)
144+
(if (equal? T1 T2)
145+
(unifiable? C)
146+
(match* (T1 T2)
147+
[(`(,T3 -> ,T4) `(,T5 -> ,T6))
148+
(unifiable? (append `((,T3 ,T5) (,T4 ,T6)) C))]
149+
[(_ _) #f]))]))
150+
|#
151+
152+
153+
154+
#|
155+
;; type Type =
156+
;; | 'Bool
157+
;; | 'Int
158+
;; | `(,Type -> ,Type)
159+
160+
;; type Expr =
161+
;; | Integer
162+
;; | Boolean
163+
;; | `(λ (,Variable : ,Type) ,Expr)
164+
;; | `(,Expr ,Expr)
165+
166+
;; TypeEnv Expr Type -> Bool
167+
(define (type-check G e T)
168+
(equal? (type-infer G e) T))
169+
170+
;; TypeEnv Expr -> (Maybe Type)
171+
(define (type-infer G e)
172+
(match e
173+
[#t 'Bool]
174+
[#f 'Bool]
175+
[(? symbol? x)
176+
(lookup x G)]
177+
[(? integer?) 'Int]
178+
[`(λ (,x : ,t) ,e)
179+
(match (type-infer (cons (list x t) G) e)
180+
[#f #f]
181+
[t2 `(,t -> ,t2)])]
182+
[`(,e0 ,e1)
183+
(match (type-infer G e0)
184+
[`(,t1 -> ,t2)
185+
(match (type-infer G e1)
186+
[#f #f]
187+
[t3 (and (equal? t1 t3) t2)])]
188+
[_ #f])]))
189+
|#
190+
191+
;; TypeEnv Expr Type -> Boolean
192+
#;
193+
(define (type-check G e T)
194+
(match e
195+
[#t (match T
196+
['Bool #t]
197+
[_ #f])]
198+
[#f (match T
199+
['Bool #t]
200+
[_ #f])]
201+
[(? integer?)
202+
(match T
203+
['Int #t]
204+
[_ #f])]
205+
206+
[(? symbol? x)
207+
(equal? (lookup x G) T)]
208+
209+
#;
210+
;; Doesn't work because we don't know what T0 should be...
211+
[`(,e0 ,e1)
212+
(and
213+
(type-check G e0 `(,T0 -> ,T))
214+
(type-check G e1 ,T0))]
215+
216+
[`(λ (,x) ,e)
217+
(match T
218+
[`(,T1 -> ,T2) (type-check (cons (list 'x T1) G) e T2)]
219+
[_ #f])]))
220+
221+
;; Variable TypeEnv -> (Maybe Type)
222+
(define (lookup x G)
223+
(match G
224+
['() #f]
225+
[(cons (list y T) G)
226+
(if (equal? x y)
227+
T
228+
(lookup x G))]))
229+
230+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
231+
232+
;; Another approach: always infer
233+
234+
;; type Type =
235+
;; | Symbol
236+
;; | 'Bool
237+
;; | 'Int
238+
;; | `(,Type -> ,Type)
239+
240+
241+
242+
243+
244+
245+
246+
247+
248+
249+
250+
251+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
252+
253+
254+
;; Another approach: type annotations, bidirectional checking
255+
256+
;; type Expr =
257+
;; | Integer
258+
;; | Boolean
259+
;; | `(λ (,Variable) ,Expr)
260+
;; | `(,Expr ,Expr)
261+
;; | `(: ,Expr ,Type)
262+
#|
263+
;; TypeEnv Expr Type -> (Maybe Type)
264+
(define (type-check G e t)
265+
(and (equal? (type-infer G e) t) t))
266+
267+
;; TypeEnv Expr -> (Maybe Type)
268+
(define (type-infer G e)
269+
(match e
270+
[#t 'Bool]
271+
[#f 'Bool]
272+
[_ #f]))
273+
274+
|#
275+
276+
277+
278+
279+
280+
281+
282+
283+
284+
285+
286+
287+
288+
289+
290+
291+
292+
293+
294+
295+
296+
297+
298+
299+
300+
301+
302+
303+
304+
305+
306+
307+
308+
309+
310+
311+
312+
313+
314+
315+
316+
317+
#|
318+
319+
;; TypeEnv Expr Type -> (Maybe Type)
320+
(define (type-check G e t)
321+
(match e
322+
[`(λ (,x) ,e)
323+
(match t
324+
[`(,t0 -> ,t1)
325+
(and (type-check (cons (list x t0) G) e t1) t)]
326+
[_ #f])]
327+
[_
328+
(and (equal? (type-infer G e) t) t)]))
329+
330+
;; TypeEnv Expr -> (Maybe Type)
331+
(define (type-infer G e)
332+
(match e
333+
[#t 'Bool]
334+
[#f 'Bool]
335+
[(? integer?) 'Int]
336+
[(? symbol? x) (lookup x G)]
337+
[`(: ,e ,t) (type-check G e t)]
338+
[`(,e0 ,e1)
339+
(match (type-infer G e0)
340+
[`(,t0 -> ,t1) (and (type-check G e1 t0) t1)]
341+
[_ #f])]
342+
[_ #f]))
343+
344+
|#
345+
346+
347+
348+
349+

0 commit comments

Comments
 (0)