Assignment 11: Type Inference
(foo y z)
(== 5 x)
Show pagesource
Log In
(foo `(,x ,y ,z) 5) (foo u v) x y z u v
> (run* q (!- ‘() #t q))
(Bool)
> (run* q (!- ‘() 17 q))
(Nat)
> (run* q (!- ‘() ‘(zero? 24) q))
(Bool)
> (run* q (!- ‘() ‘(zero? (sub1 24)) q))
(Bool)
> (run* q (!- ‘() ‘(not (zero? (sub1 24))) q))
(Bool)
> (run* q
(!- ‘() ‘(zero? (sub1 (sub1 18))) q))
(Bool)
> (run* q
(!- ‘() ‘(lambda (n) (if (zero? n) n n)) q))
((Nat -> Nat))
> (run* q
(!- ‘() ‘((lambda (n) (zero? n)) 5) q))
(Bool)
> (run* q
(!- ‘() ‘(if (zero? 24) 3 4) q))
(Nat)
> (run* q
(!- ‘() ‘(if (zero? 24) (zero? 3) (zero? 4)) q))
(Bool)
> (run* q
.hserf era dna , , , , gnimussa , erofeb emoc dluohs ,elpmaxe roF
.stnemugra detaitnatsninu htiw sllac evisrucer erofeb emoc dluohs stnemugra detaitnatsni htiw sllac evisruceR
.
erofeb emoc dluohs ,elpmaxe roF .sllac evisrucer erofeb emoc dluohs snoitacfiinu elpmiS
:dnim ni selur eseht peeK .¡±tsaf liaf¡° ot noitcnujnoc a nihtiw slaog redro ylluferac tsum uoy ,stset eht fo emos rof ecnegrevid diova oT
.ylgnidrocca snoitatcepxe eht tsujda dluohs sretteg-og laer dna stneduts sronoH .tnemngissa eht fo noitrop raluger eht rof dedivorp sesac tset eht fo lla ssap dluohs recnerefni dednetxe ruoY
.esu emos fo divaD dna ,lliW ,naD morf]fdp.sepytinim/113c/sessalc/ude.anaidni.sc.www//:ptth[seton”loohcs-dlo”gniwollofehtdnfiyamuoY
.yadseuT no ssalc ni did ew sa snoisserpxe fo sepyt eht dnah yb refni ot uoy sksa tI .maxe lanfi eht rof wonk ot deen lliw uoy lairetam stcefler tub ,dedarg eb ton lliw dna ,lanoitpo si sihT .Itrap-11a etelpmoc dna tnirp dluohs uoY
.tsal eht ni scisyhp dna suluclac neewteb taht sa luftiurf sa eb lliw yrutnec txen eht ni cigol dna noitatupmoc neewteb pihsnoitaler eht taht epoh ot elbanosaer si tI
tnemngissA
II traP
ItraP
(!- ‘() ‘(lambda (x) (sub1 x)) q))
((Nat -> Nat))
> (run* q
(!- ‘() ‘(lambda (a) (lambda (x) (+ a x))) q))
((Nat -> (Nat -> Nat)))
> (run* q
(!- ‘() ‘(lambda (f)
(lambda (x)
((f x) x)))
q))
(((_.0 -> (_.0 -> _.1)) -> (_.0 -> _.1)))
> (run* q
(!- ‘() ‘(sub1 (sub1 (sub1 6))) q))
(Nat)
> (run 1 q
(fresh (t)
(!- ‘() ‘(lambda (f) (f f)) t)))
()
> (length (run 20 (q)
(fresh (lam a b)
(!- ‘() `((,lam (,a) ,b) 5) ‘Nat)
(== `(,lam (,a) ,b) q))))
20
> (length (run 30 q (!- ‘() q ‘Nat)))
30
> (length (run 30 q (!- ‘() q ‘(Nat -> Nat))))
30
> (length (run 500 q (!- ‘() q ‘(Nat -> Nat))))
500
;; At this point, stop and take a look at maybe the 500th
;; program you generate
;; (last (run 500 q (!- ‘() q ‘(Nat -> Nat))))
;; You should be amazed at how quickly it’s generating them.
;; If it isn’t fast, consider reordering your clauses.
> (length (run 30 q (!- ‘() q ‘(Bool -> Nat))))
30
> (length (run 30 q (!- ‘() q ‘(Nat -> (Nat -> Nat)))))
30
> (length (run 100 q
(fresh (e t)
(!- ‘() e t)
(== `(,e ,t) q))))
100
> (length (run 100 q
(fresh (g e t)
(!- g e t)
(== `(,g ,e ,t) q))))
100
> (length
(run 100 q
(fresh (g v)
(!- g `(var ,v) ‘Nat)
(== `(,g ,v) q))))
100
> (run 1 q
(fresh (g)
(!- g
(Nat)
> (run 1 q
(fresh (g)
(!- g
‘((fix (lambda (!)
(lambda (n)
5) q)))
‘((fix (lambda (!)
(lambda (n)
5) q)))
(if (zero? n)
1
(* n (! (sub1 n)))))))
(* n (! (sub1 n))))))
pairof
> (run* q (!- ‘() ‘(cons (zero? 1) (zero? 0)) q))
((pairof Bool Bool))
> (run* q (!- ‘() ‘(cons (zero? 1) (cons (zero? 1) (zero? 0))) q))
((pairof Bool (pairof Bool Bool)))
> (run* t (!- ‘() ‘(lambda (x) (cons x x)) t))
((_.0 -> (pairof _.0 _.0)))
> (run* t (!- ‘() ‘(lambda (x) (lambda (y) (cons (zero? x) (+ x y)))) t))
((Nat -> (Nat -> (pairof Bool Nat))))
;; a function that accepts a pair of an Nat and anything
> (run* t (!- ‘() ‘(lambda (x) (zero? (car x))) t))
(((pairof Nat _.0) -> Bool))
> (run* t (!- ‘() ‘((lambda (x) (zero? (car x))) (cons 0 1)) t))
(Bool)
> (run* t (!- ‘() ‘((lambda (x) (zero? (car x))) (cons 0 #f)) t))
(Bool)
> (run* t (!- ‘() ‘((lambda (x) (car x)) (cons (cons 0 0) #f)) t))
((pairof Nat Nat))
> (run* t (!- ‘() ‘((lambda (x) (zero? (car x))) (cons #f 0)) t))
()
;; a function that accepts a pair of anything and an Nat
> (run* t (!- ‘() ‘(lambda (x) (zero? (cdr x))) t))
(((pairof _.0 Nat) -> Bool))
> (run* t (!- ‘() ‘((lambda (x) (zero? (cdr x))) (cons 0 1)) t))
(Bool)
> (run* t (!- ‘() ‘((lambda (x) (zero? (cdr x))) (cons 0 #f)) t))
()
> (run* t (!- ‘() ‘((lambda (x) (zero? (cdr x))) (cons #f 0)) t))
(Bool)
> (run* q
(!- ‘() ‘(let ([f (lambda (x) x)])
(if (f #t) (f (cons (f 4) 5)) (f (cons 5 (f 6)))))
q))
((pairof Nat Nat))
> (run* q
(!- ‘() ‘(let ([f (lambda (x) #t)])
q)) (Bool)
(if #t (f (f 5)) (f #t)))
(Nat) >
cvm yb 74:21 10/40/0202 :defiidom tsaL ¡¤ txt.1a-pl
:derrefni si epyt gniwollof eht taht os recnerefni epyt eht dnetxE msihpromyloP teL :tresseD tsuJ
)!rehto hcae ot ralimis etiuq eb lliw senil wen owt eseht ,yaw eht yB( .ssap stset gniwollof eht taht hcus recnerefni epyt eht ot sesualc erom owt dda ,evoba eht enod ev’uoy ecnO
.ssap stset gniwollof eht taht hcus recnerefni epyt eht ot epyt a rof troppus dda ot deen lliw uoY .sepyt riap ezingocer ot recnerefni epyt ruoy dnetxE
resaetniarB