From 6f01e1667ca73b94f2f56d7cf53064762f8a44ed Mon Sep 17 00:00:00 2001
From: David Thompson <dthompson2@worcester.edu>
Date: Sun, 8 Jan 2023 08:05:19 -0500
Subject: intersection types.

---
 infer2.scm | 43 +++++++++++++++++++++++++++++++++++++------
 1 file 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)))
 
 
 ;;;
-- 
cgit v1.2.3