Skip to content

Instantly share code, notes, and snippets.

@hcarvalhoalves
Created February 26, 2020 12:03
Show Gist options
  • Save hcarvalhoalves/041a3e6f0d3e79688e94599c371fa84d to your computer and use it in GitHub Desktop.
Save hcarvalhoalves/041a3e6f0d3e79688e94599c371fa84d to your computer and use it in GitHub Desktop.
minikanren type inference
;;; WEB -- 18 June 2016
;; Type inferencer in miniKanren, adapted from Oleg's Kanren polymorphic type inferencer
;;
;; http://kanren.cvs.sourceforge.net/viewvc/kanren/kanren/examples/type-inference.scm?view=markup
;;
;; Unlike the Kanren inferencer, this definition of !- is a pure
;; relation, with no cuts and no uses of project. This inferencer
;; also does not require a parser/unparser, and allows shadowing.
;;; TODO FIXME -- use initial environment to hold primitive functions,
;;; just like in evaluator and parser
;;; TODO -- add 'letrec', 'begin', multi-argument application,
;;; variadic and multi-argument lambda, lists, and the primitives from
;;; the evaluator
(define membero
(lambda (x ls)
(fresh (y rest)
(== `(,y . ,rest) ls)
(conde
((== y x))
((=/= y x) (membero x rest))))))
(define type-lookupo
(lambda (g x t)
(fresh (tq)
(membero `(,x . ,tq) g)
(conde
((== `(non-generic ,t) tq))
((fresh (g^ rand^)
(== `(generic ,g^ ,rand^) tq)
(!- g^ rand^ t)))))))
(define int 'int)
(define bool 'bool)
(define !-
(lambda (g expr t)
(conde
((symbolo expr) (type-lookupo g expr t))
((numbero expr) (== int t))
((== #f expr) (== bool t))
((== #t expr) (== bool t))
((fresh (e)
(== `(zero? ,e) expr)
(== bool t)
(not-in-envo 'zero? g)
(!- g e int)))
((fresh (e)
(== `(sub1 ,e) expr)
(== int t)
(not-in-envo 'sub1 g)
(!- g e int)))
((fresh (e1 e2)
(== `(+ ,e1 ,e2) expr)
(== int t)
(not-in-envo '+ g)
(!- g e1 int)
(!- g e2 int)))
((fresh (e1 e2 e3)
(== `(if ,e1 ,e2 ,e3) expr)
(not-in-envo 'if g)
(!- g e1 bool)
(!- g e2 t)
(!- g e3 t)))
((fresh (x body t-x t-body)
(== `(lambda (,x) ,body) expr)
(symbolo x)
(== `(-> ,t-x ,t-body) t)
(not-in-envo 'lambda g)
(!- `((,x non-generic ,t-x) . ,g) body t-body)))
((fresh (rator rand t-rand)
(== `(,rator ,rand) expr)
(!- g rator `(-> ,t-rand ,t))
(!- g rand t-rand)))
((fresh (rand)
(== `(fix ,rand) expr)
(not-in-envo 'fix g)
(!- g rand `(-> ,t ,t))))
((fresh (x rand body)
;; polylet
(== `(let ((,x ,rand)) ,body) expr)
(not-in-envo 'let g)
(fresh (some-type)
(!- g rand some-type))
(!- `((,x generic ,g ,rand) . ,g) body t))))))
;;; reused definitions from interpreter:
(define empty-env '())
(define (not-in-envo x env)
(conde
((== empty-env env))
((fresh (y b rest)
(== `((,y . ,b) . ,rest) env)
(=/= y x)
(not-in-envo x rest)))))
;;; tests
(test 'test-!-1
(and
(equal?
(run* (q) (!- '() '17 int))
'(_.0))
(equal?
(run* (q) (!- '() '17 q))
'(int)))
#t)
(test 'arithmetic-primitives
(run* (q) (!- '() '(zero? 24) q))
'(bool))
(test 'test-!-sub1
(run* (q) (!- '() '(zero? (sub1 24)) q))
'(bool))
(test 'test-!-+
(run* (q)
(!- '() '(zero? (sub1 (+ 18 (+ 24 50)))) q))
'(bool))
(test 'test-!-2
(and
(equal?
(run* (q) (!- '() '(zero? 24) q))
'(bool))
(equal?
(run* (q) (!- '() '(zero? (+ 24 50)) q))
'(bool))
(equal?
(run* (q)
(!- '() '(zero? (sub1 (+ 18 (+ 24 50)))) q))
'(bool)))
#t)
(test 'test-!-3
(run* (q) (!- '() '(if (zero? 24) 3 4) q))
'(int))
(test 'if-expressions
(run* (q)
(!- '() '(if (zero? 24) (zero? 3) (zero? 4)) q))
'(bool))
(test 'variables
(and
(equal?
(run* (q)
(type-lookupo '((b non-generic int) (a non-generic bool)) 'a q))
'(bool))
(equal?
(run* (q)
(!- '((a non-generic int)) '(zero? a) q))
'(bool))
(equal?
(run* (q)
(!- '((b non-generic bool) (a non-generic int))
'(zero? a)
q))
'(bool)))
#t)
(test 'variables-4a
(run* (q)
(!- '((b non-generic bool) (a non-generic int))
'(lambda (x) (+ x 5))
q))
'((-> int int)))
(test 'variables-4b
(run* (q)
(!- '((b non-generic bool) (a non-generic int))
'(lambda (x) (+ x a))
q))
'((-> int int)))
(test 'variables-4c
(run* (q)
(!- '() '(lambda (a) (lambda (x) (+ x a))) q))
'((-> int (-> int int))))
(test 'everything-but-polymorphic-let
(run* (q)
(!- '() '(lambda (f)
(lambda (x)
((f x) x)))
q))
'((->
(-> _.0 (-> _.0 _.1))
(-> _.0 _.1))))
(test 'everything-but-polymorphic-let
(run* (q)
(!- '()
'((fix (lambda (sum)
(lambda (n)
(if (zero? n)
0
(+ n (sum (sub1 n)))))))
10)
q))
'(int))
(test 'everything-but-polymorphic-let
(run* (q)
(!- '()
'((fix (lambda (sum)
(lambda (n)
(+ n (sum (sub1 n))))))
10)
q))
'(int))
(test 'everything-but-polymorphic-let
(run* (q)
(!- '()
'((lambda (f)
(if (f (zero? 5))
(+ (f 4) 8)
(+ (f 3) 7)))
(lambda (x) x))
q))
'())
(test 'polymorphic-let
(run* (q)
(!- '()
'(let ((f (lambda (x) x)))
(if (f (zero? 5))
(+ (f 4) 8)
(+ (f 3) 7)))
q))
'(int))
(test 'with-robust-syntax
(run* (q)
(!- '()
'((fix
(lambda (sum)
(lambda (n)
(if (if (zero? n) #t #f)
0
(+ n (sum (sub1 n)))))))
10)
q))
'(int))
(test 'with-robust-syntax-but-long-jumps/poly-let
(run* (q)
(!- '()
'(let ((f (lambda (x) x)))
(if (f (zero? 5))
(+ (f 4) 8)
(+ (f 3) 7)))
q))
'(int))
(test 'type-habitation-1
(run 1 (g e)
(!- g e '(-> int int)))
'(((((_.0 non-generic (-> int int)) . _.1) _.0) (sym _.0))))
(test 'type-habitation-2
(run 1 (g h r q z y t)
(!- g `(,h ,r (,q ,z ,y)) t))
'(((()
+
_.0
+
_.1
_.2
int)
(num _.0 _.1 _.2)))
)
(test 'type-habitation-2b
(run 1 (g h r q z y t)
(symbolo r)
(!- g `(,h ,r (,q ,z ,y)) t))
'(((((_.0 non-generic int))
+
_.0
+
_.1
_.2
int)
(=/= ((_.0 +)))
(num _.1 _.2)
(sym _.0)))
)
(test 'type-habitation-3
(and
(equal?
(run 1 (la f b)
(!- '() `(,la (,f) ,b) '(-> int int)))
'(((lambda _.0 _.1) (num _.1) (sym _.0))))
(equal?
(run 1 (expr type)
(fresh (h r q z y t u v)
(== `(,h ,r (,q ,z ,y)) expr)
(== `(,t ,u ,v) type)
(!- '() expr type)))
'((((lambda (_.0) (+ _.1 _.2)) (-> _.3 int))
(=/= ((_.0 +)))
(num _.1 _.2)
(sym _.0)))))
#t)
;;; Will's tests
;;; adapted from:
;;;
;;; Polymorphic Types
;;; and Type Inference Programming Languages CS442
;;; David Toman
;;; School of Computer Science University of Waterloo
;;;
;;; https://cs.uwaterloo.ca/~david/cs442/lect-TYPEINFERENCE.pdf
(test 'w-let-poly-1
(run* (q)
(!- '()
'(let ((d (lambda (f) (lambda (x) (f (f x))))))
(let ((a1 ((d (lambda (x) (sub1 x))) 2)))
(let ((a2 ((d (lambda (x) (if x #t #f))) #t)))
d)))
q))
'((-> (-> _.0 _.0) (-> _.0 _.0))))
(test 'w-let-poly-2
(run* (q)
(!- '()
'(let ((d (lambda (f) (lambda (x) (f (f x))))))
(let ((a1 ((d (lambda (x) (sub1 x))) 2)))
(let ((a2 (d (lambda (x) (if x #t #f)))))
a1)))
q))
'(int))
(test 'w-let-poly-3
(run* (q)
(!- '()
'(let ((d (lambda (f) (lambda (x) (f (f x))))))
(let ((a1 ((d (lambda (x) (sub1 x))) 2)))
(let ((a2 (d (lambda (x) (if x #t #f)))))
a2)))
q))
'((-> bool bool)))
(test 'w-let-poly-4
(run* (q)
(!- '()
'(let ((d (lambda (f) (lambda (x) (f (f x))))))
(let ((a1 ((d (lambda (x) (sub1 x))) 2)))
(let ((a2 ((d (lambda (x) (if x #t #f))) #t)))
a2)))
q))
'(bool))
#|
;; need to add lists
(test 'w-length-1
(run* (q)
(!- '()
'((fix
(lambda (length)
(lambda (l)
(if (if (null? l) #t #f)
0
(+ 1 (length (cdr l)))))))
(cons 1 (cons 2 (cons 3))))
q))
'(int))
|#
(test 'polymorphic-let-monomorphic-a
(run* (q)
(!- '()
'((lambda (g)
(let ((f (lambda (x) (g x))))
(if (f (zero? 5))
(+ (f 4) 8)
(+ (f 3) 7))))
(lambda (y) y))
q))
'())
(test 'polymorphic-let-monomorphic-b
(run* (q)
(!- '()
'((lambda (g)
(let ((f (lambda (x) x)))
(if (f (zero? 5))
(+ (f 4) 8)
(+ (f 3) 7))))
(lambda (y) y))
q))
'(int))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment