summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDavid Thompson <dthompson2@worcester.edu>2023-01-08 08:05:19 -0500
committerDavid Thompson <dthompson2@worcester.edu>2023-06-08 08:14:41 -0400
commit6f01e1667ca73b94f2f56d7cf53064762f8a44ed (patch)
tree0ad116a0594a03c4bccdf0a7064b4e58bb98f9d0
parent519b3ec07265d65900707830ae439afa01137481 (diff)
intersection types.
-rw-r--r--infer2.scm43
1 files changed, 37 insertions, 6 deletions
diff --git a/infer2.scm b/infer2.scm
index 015f897..12b9790 100644
--- a/infer2.scm
+++ b/infer2.scm
@@ -1,3 +1,7 @@
+;; features:
+;; - multiple return values
+;; - for all types
+;; - intersection types (operator overloading)
(use-modules (ice-9 format)
(ice-9 match)
(srfi srfi-1)
@@ -91,20 +95,30 @@
(variables for-all-type-variables)
(type for-all-type-type))
+(define-record-type <intersection-type>
+ (make-intersection-type types)
+ intersection-type?
+ (types intersection-type-types))
+
(define (type? obj)
(or (primitive-type? obj)
(type-variable? obj)
- (procedure-type? obj)))
+ (procedure-type? obj)
+ (intersection-type? obj)))
(define (top-level-env)
- '())
+ `((+ . ,(make-intersection-type
+ (list (make-procedure-type (list int-type int-type)
+ (list int-type))
+ (make-procedure-type (list float-type float-type)
+ (list float-type)))))))
(define (lookup var env)
(let ((type (assq-ref env var)))
(cond
- ((type-variable? type) type)
+ ((type? type) type)
((for-all-type? type) (instantiate type))
- (else (error "unbound variable" var)))))
+ (else (error "unbound variable:" var)))))
(define (occurs-in? a b)
(cond
@@ -418,6 +432,11 @@
(define %unify-prompt-tag (make-prompt-tag 'unify))
+(define (call-with-unify-backtrack thunk failure-handler)
+ (call-with-prompt %unify-prompt-tag
+ thunk
+ (lambda (_k) (failure-handler))))
+
(define (unify-fail)
(pk 'unify-fail)
(abort-to-prompt %unify-prompt-tag))
@@ -474,20 +493,32 @@
(procedure-type-return-types b)
dict*))
+(define-matcher (unify:intersection (? intersection-type? a) (? type? b) dict)
+ (let loop ((types (intersection-type-types a)))
+ (match types
+ (() (unify-fail))
+ ((t . rest)
+ (call-with-prompt %unify-prompt-tag
+ (lambda ()
+ (unify t b dict))
+ (lambda (_k)
+ (loop rest)))))))
+
(define unify
(compose-matchers unify:variable-left
unify:variable-right
unify:procedures
+ unify:intersection
unify:lists
unify:constants))
(define (unify-constraints constraints)
- (call-with-prompt %unify-prompt-tag
+ (call-with-unify-backtrack
(lambda ()
(unify (map constraint-lhs constraints)
(map constraint-rhs constraints)
'()))
- (lambda (_k) #f)))
+ (lambda () #f)))
;;;